292 then show "U + V \<noteq> {}" by blast |
292 then show "U + V \<noteq> {}" by blast |
293 show "U + V \<subseteq> E" |
293 show "U + V \<subseteq> E" |
294 proof |
294 proof |
295 fix x assume "x \<in> U + V" |
295 fix x assume "x \<in> U + V" |
296 then obtain u v where "x = u + v" and |
296 then obtain u v where "x = u + v" and |
297 "u \<in> U" and "v \<in> V" .. |
297 "u \<in> U" and "v \<in> V" .. |
298 then show "x \<in> E" by simp |
298 then show "x \<in> E" by simp |
299 qed |
299 qed |
300 fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V" |
300 fix x y assume x: "x \<in> U + V" and y: "y \<in> U + V" |
301 show "x + y \<in> U + V" |
301 show "x + y \<in> U + V" |
302 proof - |
302 proof - |
303 from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" .. |
303 from x obtain ux vx where "x = ux + vx" and "ux \<in> U" and "vx \<in> V" .. |
304 moreover |
304 moreover |
305 from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" .. |
305 from y obtain uy vy where "y = uy + vy" and "uy \<in> U" and "vy \<in> V" .. |
306 ultimately |
306 ultimately |
307 have "ux + uy \<in> U" |
307 have "ux + uy \<in> U" |
308 and "vx + vy \<in> V" |
308 and "vx + vy \<in> V" |
309 and "x + y = (ux + uy) + (vx + vy)" |
309 and "x + y = (ux + uy) + (vx + vy)" |
310 using x y by (simp_all add: add_ac) |
310 using x y by (simp_all add: add_ac) |
311 then show ?thesis .. |
311 then show ?thesis .. |
312 qed |
312 qed |
313 fix a show "a \<cdot> x \<in> U + V" |
313 fix a show "a \<cdot> x \<in> U + V" |
314 proof - |
314 proof - |
315 from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" .. |
315 from x obtain u v where "x = u + v" and "u \<in> U" and "v \<in> V" .. |
316 then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V" |
316 then have "a \<cdot> u \<in> U" and "a \<cdot> v \<in> V" |
317 and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib) |
317 and "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" by (simp_all add: distrib) |
318 then show ?thesis .. |
318 then show ?thesis .. |
319 qed |
319 qed |
320 qed |
320 qed |
321 qed |
321 qed |
322 |
322 |
402 proof (rule decomp) |
402 proof (rule decomp) |
403 show "a1 \<cdot> x' \<in> lin x'" .. |
403 show "a1 \<cdot> x' \<in> lin x'" .. |
404 show "a2 \<cdot> x' \<in> lin x'" .. |
404 show "a2 \<cdot> x' \<in> lin x'" .. |
405 show "H \<inter> lin x' = {0}" |
405 show "H \<inter> lin x' = {0}" |
406 proof |
406 proof |
407 show "H \<inter> lin x' \<subseteq> {0}" |
407 show "H \<inter> lin x' \<subseteq> {0}" |
408 proof |
408 proof |
409 fix x assume x: "x \<in> H \<inter> lin x'" |
409 fix x assume x: "x \<in> H \<inter> lin x'" |
410 then obtain a where xx': "x = a \<cdot> x'" |
410 then obtain a where xx': "x = a \<cdot> x'" |
411 by blast |
411 by blast |
412 have "x = 0" |
412 have "x = 0" |
413 proof cases |
413 proof cases |
419 with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp |
419 with xx' have "inverse a \<cdot> a \<cdot> x' \<in> H" by simp |
420 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) |
420 with a and x' have "x' \<in> H" by (simp add: mult_assoc2) |
421 with `x' \<notin> H` show ?thesis by contradiction |
421 with `x' \<notin> H` show ?thesis by contradiction |
422 qed |
422 qed |
423 then show "x \<in> {0}" .. |
423 then show "x \<in> {0}" .. |
424 qed |
424 qed |
425 show "{0} \<subseteq> H \<inter> lin x'" |
425 show "{0} \<subseteq> H \<inter> lin x'" |
426 proof - |
426 proof - |
427 have "0 \<in> H" using `vectorspace E` .. |
427 have "0 \<in> H" using `vectorspace E` .. |
428 moreover have "0 \<in> lin x'" using `x' \<in> E` .. |
428 moreover have "0 \<in> lin x'" using `x' \<in> E` .. |
429 ultimately show ?thesis by blast |
429 ultimately show ?thesis by blast |
430 qed |
430 qed |
431 qed |
431 qed |
432 show "lin x' \<unlhd> E" using `x' \<in> E` .. |
432 show "lin x' \<unlhd> E" using `x' \<in> E` .. |
433 qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) |
433 qed (rule `vectorspace E`, rule `subspace H E`, rule y1, rule y2, rule eq) |
434 then show "y1 = y2" .. |
434 then show "y1 = y2" .. |
435 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. |
435 from c have "a1 \<cdot> x' = a2 \<cdot> x'" .. |