equal
deleted
inserted
replaced
418 |
418 |
419 lemma decomp_H0_H: |
419 lemma decomp_H0_H: |
420 "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E; |
420 "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E; |
421 x0 ~= 00 |] |
421 x0 ~= 00 |] |
422 ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))" |
422 ==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))" |
423 proof (rule, unfold split_paired_all) |
423 proof (rule, unfold split_tupled_all) |
424 assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E" |
424 assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E" |
425 "x0 ~= 00" |
425 "x0 ~= 00" |
426 have h: "is_vectorspace H" .. |
426 have h: "is_vectorspace H" .. |
427 fix y a presume t1: "t = y + a (*) x0" and "y:H" |
427 fix y a presume t1: "t = y + a (*) x0" and "y:H" |
428 have "y = t & a = (#0::real)" |
428 have "y = t & a = (#0::real)" |
457 assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa" |
457 assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa" |
458 "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya" |
458 "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya" |
459 show "xa = ya" |
459 show "xa = ya" |
460 proof - |
460 proof - |
461 show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" |
461 show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" |
462 by (rule Pair_fst_snd_eq [RS iffD2]) |
462 by (simp add: Pair_fst_snd_eq) |
463 have x: "x = fst xa + snd xa (*) x0 & fst xa : H" |
463 have x: "x = fst xa + snd xa (*) x0 & fst xa : H" |
464 by (force!) |
464 by (force!) |
465 have y: "x = fst ya + snd ya (*) x0 & fst ya : H" |
465 have y: "x = fst ya + snd ya (*) x0 & fst ya : H" |
466 by (force!) |
466 by (force!) |
467 from x y show "fst xa = fst ya & snd xa = snd ya" |
467 from x y show "fst xa = fst ya & snd xa = snd ya" |