author  wenzelm 
Sun, 16 Jul 2000 20:59:06 +0200  
changeset 9370  cccba6147dae 
parent 9035  371f023d3dbd 
child 9374  153853af318b 
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 

19 
is_subspace :: "['a::{minus, plus} set, 'a set] => bool" 

7978  20 
"is_subspace U V == U ~= {} & U <= V 
9035  21 
& (ALL x:U. ALL y:U. ALL a. x + y : U & a (*) x : U)" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

22 

7566  23 
lemma subspaceI [intro]: 
8703  24 
"[ 00 : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
25 
ALL x:U. ALL a. a (*) x : U ] 

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

28 
assume "00 : U" thus "U ~= {}" by fast 

29 
qed (simp+) 

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

30 

9035  31 
lemma subspace_not_empty [intro??]: "is_subspace U V ==> U ~= {}" 
32 
by (unfold is_subspace_def) simp 

7566  33 

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

7566  36 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

37 
lemma subspace_subsetD [simp, intro??]: 
9035  38 
"[ is_subspace U V; x:U ] ==> x:V" 
39 
by (unfold is_subspace_def) force 

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

40 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

41 
lemma subspace_add_closed [simp, intro??]: 
9035  42 
"[ is_subspace U V; x:U; y:U ] ==> x + y : U" 
43 
by (unfold is_subspace_def) simp 

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

44 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

45 
lemma subspace_mult_closed [simp, intro??]: 
9035  46 
"[ is_subspace U V; x:U ] ==> a (*) x : U" 
47 
by (unfold is_subspace_def) simp 

7808  48 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

49 
lemma subspace_diff_closed [simp, intro??]: 
7978  50 
"[ is_subspace U V; is_vectorspace V; x:U; y:U ] 
9035  51 
==> x  y : U" 
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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

58 
lemma zero_in_subspace [intro??]: 
9035  59 
"[ is_subspace U V; is_vectorspace V ] ==> 00 : U" 
60 
proof  

61 
assume "is_subspace U V" and v: "is_vectorspace V" 

62 
have "U ~= {}" .. 

63 
hence "EX x. x:U" by force 

64 
thus ?thesis 

65 
proof 

66 
fix x assume u: "x:U" 

67 
hence "x:V" by (simp!) 

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

69 
also have "... : U" by (rule subspace_diff_closed) 

70 
finally show ?thesis . 

71 
qed 

72 
qed 

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

73 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

74 
lemma subspace_neg_closed [simp, intro??]: 
9035  75 
"[ is_subspace U V; is_vectorspace V; x:U ] ==>  x : U" 
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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

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 

87 
show "00 : U" .. 

88 
show "ALL x:U. ALL a. a (*) x : U" by (simp!) 

89 
show "ALL x:U. ALL y:U. x + y : U" by (simp!) 

90 
show "ALL x:U.  x = #1 (*) x" by (simp! add: negate_eq1) 

91 
show "ALL x:U. ALL y:U. x  y = x +  y" 

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" 

101 
show "00 : V" .. 

102 
show "V <= V" .. 

103 
show "ALL x:V. ALL y:V. x + y : V" by (simp!) 

104 
show "ALL x:V. ALL a. a (*) x : V" by (simp!) 

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" 

114 
show "00 : U" .. 

7656  115 

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

118 
finally show "U <= W" . 

7656  119 

9035  120 
show "ALL x:U. ALL y:U. x + y : U" 
121 
proof (intro ballI) 

122 
fix x y assume "x:U" "y:U" 

123 
show "x + y : U" by (simp!) 

124 
qed 

7656  125 

9035  126 
show "ALL x:U. ALL a. a (*) x : U" 
127 
proof (intro ballI allI) 

128 
fix x a assume "x:U" 

129 
show "a (*) x : U" by (simp!) 

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 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

141 
lin :: "'a => 'a set" 
9035  142 
"lin x == {a (*) x  a. True}" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

143 

9035  144 
lemma linD: "x : lin v = (EX a::real. x = a (*) v)" 
145 
by (unfold lin_def) fast 

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

146 

9035  147 
lemma linI [intro??]: "a (*) x0 : lin x0" 
148 
by (unfold lin_def) fast 

7656  149 

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

9035  152 
lemma x_lin_x: "[ is_vectorspace V; x:V ] ==> x : lin x" 
153 
proof (unfold lin_def, intro CollectI exI conjI) 

154 
assume "is_vectorspace V" "x:V" 

155 
show "x = #1 (*) x" by (simp!) 

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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

160 
lemma lin_subspace [intro??]: 
9035  161 
"[ is_vectorspace V; x:V ] ==> is_subspace (lin x) V" 
162 
proof 

163 
assume "is_vectorspace V" "x:V" 

164 
show "00 : lin x" 

165 
proof (unfold lin_def, intro CollectI exI conjI) 

166 
show "00 = (#0::real) (*) x" by (simp!) 

167 
qed simp 

7566  168 

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

171 
fix xa a assume "xa = a (*) x" 

172 
show "xa:V" by (simp!) 

173 
qed 

7566  174 

9035  175 
show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x" 
176 
proof (intro ballI) 

177 
fix x1 x2 assume "x1 : lin x" "x2 : lin x" 

178 
thus "x1 + x2 : lin x" 

7978  179 
proof (unfold lin_def, elim CollectE exE conjE, 
9035  180 
intro CollectI exI conjI) 
181 
fix a1 a2 assume "x1 = a1 (*) x" "x2 = a2 (*) x" 

182 
show "x1 + x2 = (a1 + a2) (*) x" 

183 
by (simp! add: vs_add_mult_distrib2) 

184 
qed simp 

185 
qed 

7566  186 

9035  187 
show "ALL xa:lin x. ALL a. a (*) xa : lin x" 
188 
proof (intro ballI allI) 

189 
fix x1 a assume "x1 : lin x" 

190 
thus "a (*) x1 : lin x" 

7978  191 
proof (unfold lin_def, elim CollectE exE conjE, 
9035  192 
intro CollectI exI conjI) 
193 
fix a1 assume "x1 = a1 (*) x" 

194 
show "a (*) x1 = (a * a1) (*) x" by (simp!) 

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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

201 
lemma lin_vs [intro??]: 
9035  202 
"[ is_vectorspace V; x:V ] ==> is_vectorspace (lin x)" 
203 
proof (rule subspace_vs) 

204 
assume "is_vectorspace V" "x:V" 

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: 

9035  218 
"U + V == {u + v  u v. u:U & v:V}" (*** 
7917  219 

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

220 
constdefs 
7917  221 
vs_sum :: 
222 
"['a::{minus, plus} set, 'a set] => 'a set" (infixl "+" 65) 

223 
"vs_sum U V == {x. EX u:U. EX v:V. x = u + v}"; 

224 
***) 

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

225 

7917  226 
lemma vs_sumD: 
9035  227 
"x: U + V = (EX u:U. EX v:V. x = u + v)" 
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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

232 
lemma vs_sumI [intro??]: 
9035  233 
"[ x:U; y:V; t= x + y ] ==> t : U + V" 
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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

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" 

243 
show "00 : U" .. 

244 
show "U <= U + V" 

245 
proof (intro subsetI vs_sumI) 

246 
fix x assume "x:U" 

247 
show "x = x + 00" by (simp!) 

248 
show "00 : V" by (simp!) 

249 
qed 

250 
show "ALL x:U. ALL y:U. x + y : U" 

251 
proof (intro ballI) 

252 
fix x y assume "x:U" "y:U" show "x + y : U" by (simp!) 

253 
qed 

254 
show "ALL x:U. ALL a. a (*) x : U" 

255 
proof (intro ballI allI) 

256 
fix x a assume "x:U" show "a (*) x : U" by (simp!) 

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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

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" 

267 
show "00 : U + V" 

268 
proof (intro vs_sumI) 

269 
show "00 : U" .. 

270 
show "00 : V" .. 

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

272 
qed 

7566  273 

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

276 
fix x u v assume "u : U" "v : V" "x = u + v" 

277 
show "x:E" by (simp!) 

278 
qed 

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

279 

9035  280 
show "ALL x: U + V. ALL y: U + V. x + y : U + V" 
281 
proof (intro ballI) 

282 
fix x y assume "x : U + V" "y : U + V" 

283 
thus "x + y : U + V" 

284 
proof (elim vs_sumE bexE, intro vs_sumI) 

285 
fix ux vx uy vy 

7917  286 
assume "ux : U" "vx : V" "x = ux + vx" 
9035  287 
and "uy : U" "vy : V" "y = uy + vy" 
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 

9035  292 
show "ALL x : U + V. ALL a. a (*) x : U + V" 
293 
proof (intro ballI allI) 

294 
fix x a assume "x : U + V" 

295 
thus "a (*) x : U + V" 

296 
proof (elim vs_sumE bexE, intro vs_sumI) 

297 
fix a x u v assume "u : U" "v : V" "x = u + v" 

298 
show "a (*) x = (a (*) u) + (a (*) v)" 

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 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
8169
diff
changeset

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; 

8703  326 
U Int V = {00}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 ] 
9035  327 
==> u1 = u2 & v1 = v2" 
328 
proof 

7808  329 
assume "is_vectorspace E" "is_subspace U E" "is_subspace V E" 
8703  330 
"U Int V = {00}" "u1:U" "u2:U" "v1:V" "v2:V" 
9035  331 
"u1 + v1 = u2 + v2" 
332 
have eq: "u1  u2 = v2  v1" by (simp! add: vs_add_diff_swap) 

333 
have u: "u1  u2 : U" by (simp!) 

334 
with eq have v': "v2  v1 : U" by simp 

335 
have v: "v2  v1 : V" by (simp!) 

336 
with eq have u': "u1  u2 : V" by simp 

7656  337 

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

340 
show "u1  u2 = 00" by (rule Int_singletonD [OF _ u u']) 

341 
show "u1 : E" .. 

342 
show "u2 : E" .. 

343 
qed 

7656  344 

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

347 
show "v2  v1 = 00" by (rule Int_singletonD [OF _ v' v]) 

348 
show "v1 : E" .. 

349 
show "v2 : E" .. 

350 
qed 

351 
qed 

7656  352 

7978  353 
text {* An application of the previous lemma will be used in the proof 
354 
of the HahnBanach Theorem (see page \pageref{decompH0use}): for any 

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 

359 
lemma decomp_H0: 

360 
"[ is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 

8703  361 
x0 ~: H; x0 : E; x0 ~= 00; y1 + a1 (*) x0 = y2 + a2 (*) x0 ] 
9035  362 
==> y1 = y2 & a1 = a2" 
363 
proof 

7656  364 
assume "is_vectorspace E" and h: "is_subspace H E" 
8703  365 
and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= 00" 
9035  366 
"y1 + a1 (*) x0 = y2 + a2 (*) x0" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

367 

9035  368 
have c: "y1 = y2 & a1 (*) x0 = a2 (*) x0" 
369 
proof (rule decomp) 

370 
show "a1 (*) x0 : lin x0" .. 

371 
show "a2 (*) x0 : lin x0" .. 

372 
show "H Int (lin x0) = {00}" 

373 
proof 

374 
show "H Int lin x0 <= {00}" 

375 
proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]) 

376 
fix x assume "x:H" "x : lin x0" 

377 
thus "x = 00" 

378 
proof (unfold lin_def, elim CollectE exE conjE) 

379 
fix a assume "x = a (*) x0" 

380 
show ?thesis 

381 
proof cases 

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

383 
next 

384 
assume "a ~= (#0::real)" 

385 
from h have "rinv a (*) a (*) x0 : H" 

386 
by (rule subspace_mult_closed) (simp!) 

387 
also have "rinv a (*) a (*) x0 = x0" by (simp!) 

388 
finally have "x0 : H" . 

389 
thus ?thesis by contradiction 

390 
qed 

391 
qed 

392 
qed 

393 
show "{00} <= H Int lin x0" 

394 
proof  

395 
have "00: H Int lin x0" 

396 
proof (rule IntI) 

397 
show "00:H" .. 

398 
from lin_vs show "00 : lin x0" .. 

399 
qed 

400 
thus ?thesis by simp 

401 
qed 

402 
qed 

403 
show "is_subspace (lin x0) E" .. 

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]) 

410 
from c show "a1 (*) x0 = a2 (*) x0" by simp 

411 
qed 

412 
qed 

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

413 

7978  414 
text {* Since for any element $y + a \mult x_0$ of the direct sum 
7917  415 
of a vectorspace $H$ and the linear closure of $x_0$ the components 
7978  416 
$y\in H$ and $a$ are unique, it follows from $y\in H$ that 
9035  417 
$a = 0$.*} 
7917  418 

419 
lemma decomp_H0_H: 

7978  420 
"[ is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E; 
8703  421 
x0 ~= 00 ] 
9035  422 
==> (SOME (y, a). t = y + a (*) x0 & y : H) = (t, (#0::real))" 
9370  423 
proof (rule, unfold split_tupled_all) 
7978  424 
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E" 
9035  425 
"x0 ~= 00" 
426 
have h: "is_vectorspace H" .. 

427 
fix y a presume t1: "t = y + a (*) x0" and "y:H" 

428 
have "y = t & a = (#0::real)" 

429 
by (rule decomp_H0) (assumption  (simp!))+ 

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 

7917  433 
text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
434 
are unique, so the function $h_0$ defined by 

9035  435 
$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *} 
7917  436 

437 
lemma h0_definite: 

8703  438 
"[ h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) 
7566  439 
in (h y) + a * xi); 
8703  440 
x = y + a (*) x0; is_vectorspace E; is_subspace H E; 
441 
y:H; x0 ~: H; x0:E; x0 ~= 00 ] 

9035  442 
==> h0 x = h y + a * xi" 
443 
proof  

7917  444 
assume 
8703  445 
"h0 == (\\<lambda>x. let (y, a) = SOME (y, a). (x = y + a (*) x0 & y:H) 
7917  446 
in (h y) + a * xi)" 
8703  447 
"x = y + a (*) x0" "is_vectorspace E" "is_subspace H E" 
9035  448 
"y:H" "x0 ~: H" "x0:E" "x0 ~= 00" 
449 
have "x : H + (lin x0)" 

450 
by (simp! add: vs_sum_def lin_def) force+ 

451 
have "EX! xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)" 

452 
proof 

453 
show "EX xa. ((\\<lambda>(y, a). x = y + a (*) x0 & y:H) xa)" 

454 
by (force!) 

455 
next 

456 
fix xa ya 

8703  457 
assume "(\\<lambda>(y,a). x = y + a (*) x0 & y : H) xa" 
9035  458 
"(\\<lambda>(y,a). x = y + a (*) x0 & y : H) ya" 
459 
show "xa = ya" 

460 
proof  

461 
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya" 

9370  462 
by (simp add: Pair_fst_snd_eq) 
9035  463 
have x: "x = fst xa + snd xa (*) x0 & fst xa : H" 
464 
by (force!) 

465 
have y: "x = fst ya + snd ya (*) x0 & fst ya : H" 

466 
by (force!) 

467 
from x y show "fst xa = fst ya & snd xa = snd ya" 

468 
by (elim conjE) (rule decomp_H0, (simp!)+) 

469 
qed 

470 
qed 

471 
hence eq: "(SOME (y, a). x = y + a (*) x0 & y:H) = (y, a)" 

472 
by (rule select1_equality) (force!) 

473 
thus "h0 x = h y + a * xi" by (simp! add: Let_def) 

474 
qed 

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

475 

9035  476 
end 