author  wenzelm 
Sun, 23 Jul 2000 12:01:05 +0200  
changeset 9408  d3d56e1d2ec1 
parent 9374  153853af318b 
child 9623  3ade112482af 
permissions  rwrr 
7566  1 
(* Title: HOL/Real/HahnBanach/Subspace.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer, TU Munich 

4 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

5 

7808  6 

9035  7 
header {* Subspaces *} 
7808  8 

9035  9 
theory Subspace = VectorSpace: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

11 

9035  12 
subsection {* Definition *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

13 

7917  14 
text {* A nonempty subset $U$ of a vector space $V$ is a 
15 
\emph{subspace} of $V$, iff $U$ is closed under addition and 

9035  16 
scalar multiplication. *} 
7917  17 

18 
constdefs 

9374  19 
is_subspace :: "['a::{plus, minus, zero} set, 'a set] => bool" 
20 
"is_subspace U V == U \<noteq> {} \<and> U <= V 

21 
\<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x\<in> U)" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

22 

7566  23 
lemma subspaceI [intro]: 
9374  24 
"[ 0 \<in> U; U <= V; \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U); 
25 
\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U ] 

9035  26 
==> is_subspace U V" 
27 
proof (unfold is_subspace_def, intro conjI) 

9374  28 
assume "0 \<in> U" thus "U \<noteq> {}" by fast 
9035  29 
qed (simp+) 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

30 

9408  31 
lemma subspace_not_empty [intro?]: "is_subspace U V ==> U \<noteq> {}" 
9035  32 
by (unfold is_subspace_def) simp 
7566  33 

9408  34 
lemma subspace_subset [intro?]: "is_subspace U V ==> U <= V" 
9035  35 
by (unfold is_subspace_def) simp 
7566  36 

9408  37 
lemma subspace_subsetD [simp, intro?]: 
9374  38 
"[ is_subspace U V; x \<in> U ] ==> x \<in> V" 
9035  39 
by (unfold is_subspace_def) force 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 

9408  41 
lemma subspace_add_closed [simp, intro?]: 
9374  42 
"[ is_subspace U V; x \<in> U; y \<in> U ] ==> x + y \<in> U" 
9035  43 
by (unfold is_subspace_def) simp 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

44 

9408  45 
lemma subspace_mult_closed [simp, intro?]: 
9374  46 
"[ is_subspace U V; x \<in> U ] ==> a \<cdot> x \<in> U" 
9035  47 
by (unfold is_subspace_def) simp 
7808  48 

9408  49 
lemma subspace_diff_closed [simp, intro?]: 
9374  50 
"[ is_subspace U V; is_vectorspace V; x \<in> U; y \<in> U ] 
51 
==> x  y \<in> U" 

9035  52 
by (simp! add: diff_eq1 negate_eq1) 
7917  53 

54 
text {* Similar as for linear spaces, the existence of the 

7978  55 
zero element in every subspace follows from the nonemptiness 
9035  56 
of the carrier set and by vector space laws.*} 
7917  57 

9408  58 
lemma zero_in_subspace [intro?]: 
9374  59 
"[ is_subspace U V; is_vectorspace V ] ==> 0 \<in> U" 
9035  60 
proof  
61 
assume "is_subspace U V" and v: "is_vectorspace V" 

9374  62 
have "U \<noteq> {}" .. 
63 
hence "\<exists>x. x \<in> U" by force 

9035  64 
thus ?thesis 
65 
proof 

9374  66 
fix x assume u: "x \<in> U" 
67 
hence "x \<in> V" by (simp!) 

68 
with v have "0 = x  x" by (simp!) 

69 
also have "... \<in> U" by (rule subspace_diff_closed) 

9035  70 
finally show ?thesis . 
71 
qed 

72 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

73 

9408  74 
lemma subspace_neg_closed [simp, intro?]: 
9374  75 
"[ is_subspace U V; is_vectorspace V; x \<in> U ] ==>  x \<in> U" 
9035  76 
by (simp add: negate_eq1) 
7917  77 

9035  78 
text_raw {* \medskip *} 
79 
text {* Further derived laws: every subspace is a vector space. *} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

80 

9408  81 
lemma subspace_vs [intro?]: 
9035  82 
"[ is_subspace U V; is_vectorspace V ] ==> is_vectorspace U" 
83 
proof  

84 
assume "is_subspace U V" "is_vectorspace V" 

85 
show ?thesis 

86 
proof 

9374  87 
show "0 \<in> U" .. 
88 
show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!) 

89 
show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!) 

90 
show "\<forall>x \<in> U.  x = #1 \<cdot> x" by (simp! add: negate_eq1) 

91 
show "\<forall>x \<in> U. \<forall>y \<in> U. x  y = x +  y" 

9035  92 
by (simp! add: diff_eq1) 
93 
qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+ 

94 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

95 

9035  96 
text {* The subspace relation is reflexive. *} 
7917  97 

9035  98 
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V" 
99 
proof 

100 
assume "is_vectorspace V" 

9374  101 
show "0 \<in> V" .. 
9035  102 
show "V <= V" .. 
9374  103 
show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!) 
104 
show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!) 

9035  105 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

106 

9035  107 
text {* The subspace relation is transitive. *} 
7917  108 

7808  109 
lemma subspace_trans: 
7917  110 
"[ is_subspace U V; is_vectorspace V; is_subspace V W ] 
9035  111 
==> is_subspace U W" 
112 
proof 

113 
assume "is_subspace U V" "is_subspace V W" "is_vectorspace V" 

9374  114 
show "0 \<in> U" .. 
7656  115 

9035  116 
have "U <= V" .. 
117 
also have "V <= W" .. 

118 
finally show "U <= W" . 

7656  119 

9374  120 
show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
9035  121 
proof (intro ballI) 
9374  122 
fix x y assume "x \<in> U" "y \<in> U" 
123 
show "x + y \<in> U" by (simp!) 

9035  124 
qed 
7656  125 

9374  126 
show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" 
9035  127 
proof (intro ballI allI) 
9374  128 
fix x a assume "x \<in> U" 
129 
show "a \<cdot> x \<in> U" by (simp!) 

9035  130 
qed 
131 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

132 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

133 

7808  134 

9035  135 
subsection {* Linear closure *} 
7808  136 

7978  137 
text {* The \emph{linear closure} of a vector $x$ is the set of all 
9035  138 
scalar multiples of $x$. *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

139 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

140 
constdefs 
9374  141 
lin :: "('a::{minus,plus,zero}) => 'a set" 
142 
"lin x == {a \<cdot> x  a. True}" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

143 

9374  144 
lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)" 
9035  145 
by (unfold lin_def) fast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

146 

9408  147 
lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0" 
9035  148 
by (unfold lin_def) fast 
7656  149 

9035  150 
text {* Every vector is contained in its linear closure. *} 
7917  151 

9374  152 
lemma x_lin_x: "[ is_vectorspace V; x \<in> V ] ==> x \<in> lin x" 
9035  153 
proof (unfold lin_def, intro CollectI exI conjI) 
9374  154 
assume "is_vectorspace V" "x \<in> V" 
155 
show "x = #1 \<cdot> x" by (simp!) 

9035  156 
qed simp 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

157 

9035  158 
text {* Any linear closure is a subspace. *} 
7917  159 

9408  160 
lemma lin_subspace [intro?]: 
9374  161 
"[ is_vectorspace V; x \<in> V ] ==> is_subspace (lin x) V" 
9035  162 
proof 
9374  163 
assume "is_vectorspace V" "x \<in> V" 
164 
show "0 \<in> lin x" 

9035  165 
proof (unfold lin_def, intro CollectI exI conjI) 
9374  166 
show "0 = (#0::real) \<cdot> x" by (simp!) 
9035  167 
qed simp 
7566  168 

9035  169 
show "lin x <= V" 
170 
proof (unfold lin_def, intro subsetI, elim CollectE exE conjE) 

9374  171 
fix xa a assume "xa = a \<cdot> x" 
172 
show "xa \<in> V" by (simp!) 

9035  173 
qed 
7566  174 

9374  175 
show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x" 
9035  176 
proof (intro ballI) 
9374  177 
fix x1 x2 assume "x1 \<in> lin x" "x2 \<in> lin x" 
178 
thus "x1 + x2 \<in> lin x" 

7978  179 
proof (unfold lin_def, elim CollectE exE conjE, 
9035  180 
intro CollectI exI conjI) 
9374  181 
fix a1 a2 assume "x1 = a1 \<cdot> x" "x2 = a2 \<cdot> x" 
182 
show "x1 + x2 = (a1 + a2) \<cdot> x" 

9035  183 
by (simp! add: vs_add_mult_distrib2) 
184 
qed simp 

185 
qed 

7566  186 

9374  187 
show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x" 
9035  188 
proof (intro ballI allI) 
9374  189 
fix x1 a assume "x1 \<in> lin x" 
190 
thus "a \<cdot> x1 \<in> lin x" 

7978  191 
proof (unfold lin_def, elim CollectE exE conjE, 
9035  192 
intro CollectI exI conjI) 
9374  193 
fix a1 assume "x1 = a1 \<cdot> x" 
194 
show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!) 

9035  195 
qed simp 
196 
qed 

197 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

198 

9035  199 
text {* Any linear closure is a vector space. *} 
7917  200 

9408  201 
lemma lin_vs [intro?]: 
9374  202 
"[ is_vectorspace V; x \<in> V ] ==> is_vectorspace (lin x)" 
9035  203 
proof (rule subspace_vs) 
9374  204 
assume "is_vectorspace V" "x \<in> V" 
9035  205 
show "is_subspace (lin x) V" .. 
206 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

207 

7808  208 

209 

9035  210 
subsection {* Sum of two vectorspaces *} 
7808  211 

7917  212 
text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of 
9035  213 
all sums of elements from $U$ and $V$. *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

214 

9035  215 
instance set :: (plus) plus by intro_classes 
7917  216 

217 
defs vs_sum_def: 

9374  218 
"U + V == {u + v  u v. u \<in> U \<and> v \<in> V}" (*** 
7917  219 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

220 
constdefs 
7917  221 
vs_sum :: 
9374  222 
"['a::{plus, minus, zero} set, 'a set] => 'a set" (infixl "+" 65) 
223 
"vs_sum U V == {x. \<exists>u \<in> U. \<exists>v \<in> V. x = u + v}"; 

7917  224 
***) 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

225 

7917  226 
lemma vs_sumD: 
9374  227 
"x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)" 
9035  228 
by (unfold vs_sum_def) fast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

229 

9035  230 
lemmas vs_sumE = vs_sumD [RS iffD1, elimify] 
7566  231 

9408  232 
lemma vs_sumI [intro?]: 
9374  233 
"[ x \<in> U; y \<in> V; t= x + y ] ==> t \<in> U + V" 
9035  234 
by (unfold vs_sum_def) fast 
7917  235 

9035  236 
text{* $U$ is a subspace of $U + V$. *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

237 

9408  238 
lemma subspace_vs_sum1 [intro?]: 
7917  239 
"[ is_vectorspace U; is_vectorspace V ] 
9035  240 
==> is_subspace U (U + V)" 
241 
proof 

242 
assume "is_vectorspace U" "is_vectorspace V" 

9374  243 
show "0 \<in> U" .. 
9035  244 
show "U <= U + V" 
245 
proof (intro subsetI vs_sumI) 

9374  246 
fix x assume "x \<in> U" 
247 
show "x = x + 0" by (simp!) 

248 
show "0 \<in> V" by (simp!) 

9035  249 
qed 
9374  250 
show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" 
9035  251 
proof (intro ballI) 
9374  252 
fix x y assume "x \<in> U" "y \<in> U" show "x + y \<in> U" by (simp!) 
9035  253 
qed 
9374  254 
show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" 
9035  255 
proof (intro ballI allI) 
9374  256 
fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!) 
9035  257 
qed 
258 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

259 

9035  260 
text{* The sum of two subspaces is again a subspace.*} 
7917  261 

9408  262 
lemma vs_sum_subspace [intro?]: 
7566  263 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 
9035  264 
==> is_subspace (U + V) E" 
265 
proof 

266 
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" 

9374  267 
show "0 \<in> U + V" 
9035  268 
proof (intro vs_sumI) 
9374  269 
show "0 \<in> U" .. 
270 
show "0 \<in> V" .. 

271 
show "(0::'a) = 0 + 0" by (simp!) 

9035  272 
qed 
7566  273 

9035  274 
show "U + V <= E" 
275 
proof (intro subsetI, elim vs_sumE bexE) 

9374  276 
fix x u v assume "u \<in> U" "v \<in> V" "x = u + v" 
277 
show "x \<in> E" by (simp!) 

9035  278 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

279 

9374  280 
show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V" 
9035  281 
proof (intro ballI) 
9374  282 
fix x y assume "x \<in> U + V" "y \<in> U + V" 
283 
thus "x + y \<in> U + V" 

9035  284 
proof (elim vs_sumE bexE, intro vs_sumI) 
285 
fix ux vx uy vy 

9374  286 
assume "ux \<in> U" "vx \<in> V" "x = ux + vx" 
287 
and "uy \<in> U" "vy \<in> V" "y = uy + vy" 

9035  288 
show "x + y = (ux + uy) + (vx + vy)" by (simp!) 
289 
qed (simp!)+ 

290 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

291 

9374  292 
show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V" 
9035  293 
proof (intro ballI allI) 
9374  294 
fix x a assume "x \<in> U + V" 
295 
thus "a \<cdot> x \<in> U + V" 

9035  296 
proof (elim vs_sumE bexE, intro vs_sumI) 
9374  297 
fix a x u v assume "u \<in> U" "v \<in> V" "x = u + v" 
298 
show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)" 

9035  299 
by (simp! add: vs_add_mult_distrib1) 
300 
qed (simp!)+ 

301 
qed 

302 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

303 

9035  304 
text{* The sum of two subspaces is a vectorspace. *} 
7917  305 

9408  306 
lemma vs_sum_vs [intro?]: 
7566  307 
"[ is_subspace U E; is_subspace V E; is_vectorspace E ] 
9035  308 
==> is_vectorspace (U + V)" 
309 
proof (rule subspace_vs) 

310 
assume "is_subspace U E" "is_subspace V E" "is_vectorspace E" 

311 
show "is_subspace (U + V) E" .. 

312 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

313 

599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

314 

7808  315 

9035  316 
subsection {* Direct sums *} 
7808  317 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

318 

7917  319 
text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
320 
element is the only common element of $U$ and $V$. For every element 

321 
$x$ of the direct sum of $U$ and $V$ the decomposition in 

9035  322 
$x = u + v$ with $u \in U$ and $v \in V$ is unique.*} 
7808  323 

7917  324 
lemma decomp: 
325 
"[ is_vectorspace E; is_subspace U E; is_subspace V E; 

9374  326 
U \<inter> V = {0}; u1 \<in> U; u2 \<in> U; v1 \<in> V; v2 \<in> V; u1 + v1 = u2 + v2 ] 
327 
==> u1 = u2 \<and> v1 = v2" 

9035  328 
proof 
7808  329 
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" 
9374  330 
"U \<inter> V = {0}" "u1 \<in> U" "u2 \<in> U" "v1 \<in> V" "v2 \<in> V" 
9035  331 
"u1 + v1 = u2 + v2" 
332 
have eq: "u1  u2 = v2  v1" by (simp! add: vs_add_diff_swap) 

9374  333 
have u: "u1  u2 \<in> U" by (simp!) 
334 
with eq have v': "v2  v1 \<in> U" by simp 

335 
have v: "v2  v1 \<in> V" by (simp!) 

336 
with eq have u': "u1  u2 \<in> V" by simp 

7656  337 

9035  338 
show "u1 = u2" 
339 
proof (rule vs_add_minus_eq) 

9374  340 
show "u1  u2 = 0" by (rule Int_singletonD [OF _ u u']) 
341 
show "u1 \<in> E" .. 

342 
show "u2 \<in> E" .. 

9035  343 
qed 
7656  344 

9035  345 
show "v1 = v2" 
346 
proof (rule vs_add_minus_eq [RS sym]) 

9374  347 
show "v2  v1 = 0" by (rule Int_singletonD [OF _ v' v]) 
348 
show "v1 \<in> E" .. 

349 
show "v2 \<in> E" .. 

9035  350 
qed 
351 
qed 

7656  352 

7978  353 
text {* An application of the previous lemma will be used in the proof 
9374  354 
of the HahnBanach Theorem (see page \pageref{decompHuse}): for any 
7978  355 
element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and 
356 
the linear closure of $x_0$ the components $y \in H$ and $a$ are 

9035  357 
uniquely determined. *} 
7917  358 

9374  359 
lemma decomp_H': 
360 
"[ is_vectorspace E; is_subspace H E; y1 \<in> H; y2 \<in> H; 

361 
x' \<notin> H; x' \<in> E; x' \<noteq> 0; y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x' ] 

362 
==> y1 = y2 \<and> a1 = a2" 

9035  363 
proof 
7656  364 
assume "is_vectorspace E" and h: "is_subspace H E" 
9374  365 
and "y1 \<in> H" "y2 \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 
366 
"y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

367 

9374  368 
have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'" 
9035  369 
proof (rule decomp) 
9374  370 
show "a1 \<cdot> x' \<in> lin x'" .. 
371 
show "a2 \<cdot> x' \<in> lin x'" .. 

372 
show "H \<inter> (lin x') = {0}" 

9035  373 
proof 
9374  374 
show "H \<inter> lin x' <= {0}" 
9035  375 
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]) 
9374  376 
fix x assume "x \<in> H" "x \<in> lin x'" 
377 
thus "x = 0" 

9035  378 
proof (unfold lin_def, elim CollectE exE conjE) 
9374  379 
fix a assume "x = a \<cdot> x'" 
9035  380 
show ?thesis 
381 
proof cases 

382 
assume "a = (#0::real)" show ?thesis by (simp!) 

383 
next 

9374  384 
assume "a \<noteq> (#0::real)" 
385 
from h have "rinv a \<cdot> a \<cdot> x' \<in> H" 

9035  386 
by (rule subspace_mult_closed) (simp!) 
9374  387 
also have "rinv a \<cdot> a \<cdot> x' = x'" by (simp!) 
388 
finally have "x' \<in> H" . 

9035  389 
thus ?thesis by contradiction 
390 
qed 

391 
qed 

392 
qed 

9374  393 
show "{0} <= H \<inter> lin x'" 
9035  394 
proof  
9374  395 
have "0 \<in> H \<inter> lin x'" 
9035  396 
proof (rule IntI) 
9374  397 
show "0 \<in> H" .. 
398 
from lin_vs show "0 \<in> lin x'" .. 

9035  399 
qed 
400 
thus ?thesis by simp 

401 
qed 

402 
qed 

9374  403 
show "is_subspace (lin x') E" .. 
9035  404 
qed 
7656  405 

9035  406 
from c show "y1 = y2" by simp 
7656  407 

9035  408 
show "a1 = a2" 
409 
proof (rule vs_mult_right_cancel [RS iffD1]) 

9374  410 
from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp 
9035  411 
qed 
412 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

413 

9374  414 
text {* Since for any element $y + a \mult x'$ of the direct sum 
415 
of a vectorspace $H$ and the linear closure of $x'$ the components 

7978  416 
$y\in H$ and $a$ are unique, it follows from $y\in H$ that 
9035  417 
$a = 0$.*} 
7917  418 

9374  419 
lemma decomp_H'_H: 
420 
"[ is_vectorspace E; is_subspace H E; t \<in> H; x' \<notin> H; x' \<in> E; 

421 
x' \<noteq> 0 ] 

422 
==> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))" 

9370  423 
proof (rule, unfold split_tupled_all) 
9374  424 
assume "is_vectorspace E" "is_subspace H E" "t \<in> H" "x' \<notin> H" "x' \<in> E" 
425 
"x' \<noteq> 0" 

9035  426 
have h: "is_vectorspace H" .. 
9374  427 
fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H" 
428 
have "y = t \<and> a = (#0::real)" 

429 
by (rule decomp_H') (assumption  (simp!))+ 

9035  430 
thus "(y, a) = (t, (#0::real))" by (simp!) 
431 
qed (simp!)+ 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

432 

9374  433 
text {* The components $y\in H$ and $a$ in $y \plus a \mult x'$ 
434 
are unique, so the function $h'$ defined by 

435 
$h' (y \plus a \mult x') = h y + a \cdot \xi$ is definite. *} 

7917  436 

9374  437 
lemma h'_definite: 
438 
"[ h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) 

7566  439 
in (h y) + a * xi); 
9374  440 
x = y + a \<cdot> x'; is_vectorspace E; is_subspace H E; 
441 
y \<in> H; x' \<notin> H; x' \<in> E; x' \<noteq> 0 ] 

442 
==> h' x = h y + a * xi" 

9035  443 
proof  
7917  444 
assume 
9374  445 
"h' == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H) 
7917  446 
in (h y) + a * xi)" 
9374  447 
"x = y + a \<cdot> x'" "is_vectorspace E" "is_subspace H E" 
448 
"y \<in> H" "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0" 

449 
have "x \<in> H + (lin x')" 

9035  450 
by (simp! add: vs_sum_def lin_def) force+ 
9374  451 
have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" 
9035  452 
proof 
9374  453 
show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)" 
9035  454 
by (force!) 
455 
next 

456 
fix xa ya 

9374  457 
assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa" 
458 
"(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya" 

9035  459 
show "xa = ya" 
460 
proof  

9374  461 
show "fst xa = fst ya \<and> snd xa = snd ya ==> xa = ya" 
9370  462 
by (simp add: Pair_fst_snd_eq) 
9374  463 
have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H" 
9035  464 
by (force!) 
9374  465 
have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H" 
9035  466 
by (force!) 
9374  467 
from x y show "fst xa = fst ya \<and> snd xa = snd ya" 
468 
by (elim conjE) (rule decomp_H', (simp!)+) 

9035  469 
qed 
470 
qed 

9374  471 
hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)" 
9035  472 
by (rule select1_equality) (force!) 
9374  473 
thus "h' x = h y + a * xi" by (simp! add: Let_def) 
9035  474 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

475 

9035  476 
end 