src/HOL/Real/HahnBanach/Subspace.thy
author wenzelm
Sat Dec 16 21:41:51 2000 +0100 (2000-12-16)
changeset 10687 c186279eecea
parent 10606 e3229a37d53f
child 11655 923e4d0d36d5
permissions -rw-r--r--
tuned HOL/Real/HahnBanach;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Subspace.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@9035
     6
header {* Subspaces *}
wenzelm@7808
     7
wenzelm@9035
     8
theory Subspace = VectorSpace:
wenzelm@7535
     9
wenzelm@7535
    10
wenzelm@9035
    11
subsection {* Definition *}
wenzelm@7535
    12
wenzelm@10687
    13
text {*
wenzelm@10687
    14
  A non-empty subset @{text U} of a vector space @{text V} is a
wenzelm@10687
    15
  \emph{subspace} of @{text V}, iff @{text U} is closed under addition
wenzelm@10687
    16
  and scalar multiplication.
wenzelm@10687
    17
*}
wenzelm@7917
    18
wenzelm@10687
    19
constdefs
wenzelm@10687
    20
  is_subspace ::  "'a::{plus, minus, zero} set \<Rightarrow> 'a set \<Rightarrow> bool"
wenzelm@10687
    21
  "is_subspace U V \<equiv> U \<noteq> {} \<and> U \<subseteq> V
wenzelm@10687
    22
     \<and> (\<forall>x \<in> U. \<forall>y \<in> U. \<forall>a. x + y \<in> U \<and> a \<cdot> x \<in> U)"
wenzelm@7535
    23
wenzelm@10687
    24
lemma subspaceI [intro]:
wenzelm@10687
    25
  "0 \<in> U \<Longrightarrow> U \<subseteq> V \<Longrightarrow> \<forall>x \<in> U. \<forall>y \<in> U. (x + y \<in> U) \<Longrightarrow>
wenzelm@10687
    26
  \<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U
wenzelm@10687
    27
  \<Longrightarrow> is_subspace U V"
wenzelm@10687
    28
proof (unfold is_subspace_def, intro conjI)
bauerg@9374
    29
  assume "0 \<in> U" thus "U \<noteq> {}" by fast
wenzelm@9035
    30
qed (simp+)
wenzelm@7535
    31
wenzelm@10687
    32
lemma subspace_not_empty [intro?]: "is_subspace U V \<Longrightarrow> U \<noteq> {}"
wenzelm@10687
    33
  by (unfold is_subspace_def) blast
wenzelm@7566
    34
wenzelm@10687
    35
lemma subspace_subset [intro?]: "is_subspace U V \<Longrightarrow> U \<subseteq> V"
wenzelm@10687
    36
  by (unfold is_subspace_def) blast
wenzelm@7566
    37
wenzelm@10687
    38
lemma subspace_subsetD [simp, intro?]:
wenzelm@10687
    39
  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> x \<in> V"
wenzelm@10687
    40
  by (unfold is_subspace_def) blast
wenzelm@7535
    41
wenzelm@10687
    42
lemma subspace_add_closed [simp, intro?]:
wenzelm@10687
    43
  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x + y \<in> U"
wenzelm@10687
    44
  by (unfold is_subspace_def) blast
wenzelm@7535
    45
wenzelm@10687
    46
lemma subspace_mult_closed [simp, intro?]:
wenzelm@10687
    47
  "is_subspace U V \<Longrightarrow> x \<in> U \<Longrightarrow> a \<cdot> x \<in> U"
wenzelm@10687
    48
  by (unfold is_subspace_def) blast
wenzelm@7808
    49
wenzelm@10687
    50
lemma subspace_diff_closed [simp, intro?]:
wenzelm@10687
    51
  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> y \<in> U
wenzelm@10687
    52
  \<Longrightarrow> x - y \<in> U"
wenzelm@10687
    53
  by (simp add: diff_eq1 negate_eq1)
wenzelm@7917
    54
wenzelm@10687
    55
text {* Similar as for linear spaces, the existence of the
wenzelm@10687
    56
zero element in every subspace follows from the non-emptiness
wenzelm@9035
    57
of the carrier set and by vector space laws.*}
wenzelm@7917
    58
wenzelm@9408
    59
lemma zero_in_subspace [intro?]:
wenzelm@10687
    60
  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> 0 \<in> U"
wenzelm@10687
    61
proof -
wenzelm@9035
    62
  assume "is_subspace U V" and v: "is_vectorspace V"
bauerg@9374
    63
  have "U \<noteq> {}" ..
wenzelm@10687
    64
  hence "\<exists>x. x \<in> U" by blast
wenzelm@10687
    65
  thus ?thesis
wenzelm@10687
    66
  proof
wenzelm@10687
    67
    fix x assume u: "x \<in> U"
bauerg@9374
    68
    hence "x \<in> V" by (simp!)
bauerg@9374
    69
    with v have "0 = x - x" by (simp!)
bauerg@9374
    70
    also have "... \<in> U" by (rule subspace_diff_closed)
wenzelm@9035
    71
    finally show ?thesis .
wenzelm@9035
    72
  qed
wenzelm@9035
    73
qed
wenzelm@7535
    74
wenzelm@10687
    75
lemma subspace_neg_closed [simp, intro?]:
wenzelm@10687
    76
  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> x \<in> U \<Longrightarrow> - x \<in> U"
wenzelm@9035
    77
  by (simp add: negate_eq1)
wenzelm@7917
    78
wenzelm@10687
    79
text {* \medskip Further derived laws: every subspace is a vector space. *}
wenzelm@7535
    80
wenzelm@9408
    81
lemma subspace_vs [intro?]:
wenzelm@10687
    82
  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_vectorspace U"
wenzelm@9035
    83
proof -
wenzelm@10687
    84
  assume "is_subspace U V"  "is_vectorspace V"
wenzelm@9035
    85
  show ?thesis
wenzelm@10687
    86
  proof
bauerg@9374
    87
    show "0 \<in> U" ..
bauerg@9374
    88
    show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U" by (simp!)
bauerg@9374
    89
    show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U" by (simp!)
bauerg@9374
    90
    show "\<forall>x \<in> U. - x = -#1 \<cdot> x" by (simp! add: negate_eq1)
wenzelm@10687
    91
    show "\<forall>x \<in> U. \<forall>y \<in> U. x - y =  x + - y"
wenzelm@9035
    92
      by (simp! add: diff_eq1)
wenzelm@9035
    93
  qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+
wenzelm@9035
    94
qed
wenzelm@7535
    95
wenzelm@9035
    96
text {* The subspace relation is reflexive. *}
wenzelm@7917
    97
wenzelm@10687
    98
lemma subspace_refl [intro]: "is_vectorspace V \<Longrightarrow> is_subspace V V"
wenzelm@10687
    99
proof
wenzelm@9035
   100
  assume "is_vectorspace V"
bauerg@9374
   101
  show "0 \<in> V" ..
wenzelm@10687
   102
  show "V \<subseteq> V" ..
bauerg@9374
   103
  show "\<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V" by (simp!)
bauerg@9374
   104
  show "\<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V" by (simp!)
wenzelm@9035
   105
qed
wenzelm@7535
   106
wenzelm@9035
   107
text {* The subspace relation is transitive. *}
wenzelm@7917
   108
wenzelm@10687
   109
lemma subspace_trans:
wenzelm@10687
   110
  "is_subspace U V \<Longrightarrow> is_vectorspace V \<Longrightarrow> is_subspace V W
wenzelm@10687
   111
  \<Longrightarrow> is_subspace U W"
wenzelm@10687
   112
proof
wenzelm@10687
   113
  assume "is_subspace U V"  "is_subspace V W"  "is_vectorspace V"
bauerg@9374
   114
  show "0 \<in> U" ..
wenzelm@7656
   115
wenzelm@10687
   116
  have "U \<subseteq> V" ..
wenzelm@10687
   117
  also have "V \<subseteq> W" ..
wenzelm@10687
   118
  finally show "U \<subseteq> W" .
wenzelm@7656
   119
wenzelm@10687
   120
  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
wenzelm@9035
   121
  proof (intro ballI)
wenzelm@10687
   122
    fix x y assume "x \<in> U"  "y \<in> U"
bauerg@9374
   123
    show "x + y \<in> U" by (simp!)
wenzelm@9035
   124
  qed
wenzelm@7656
   125
bauerg@9374
   126
  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
wenzelm@9035
   127
  proof (intro ballI allI)
bauerg@9374
   128
    fix x a assume "x \<in> U"
bauerg@9374
   129
    show "a \<cdot> x \<in> U" by (simp!)
wenzelm@9035
   130
  qed
wenzelm@9035
   131
qed
wenzelm@7535
   132
wenzelm@7535
   133
wenzelm@7808
   134
wenzelm@9035
   135
subsection {* Linear closure *}
wenzelm@7808
   136
wenzelm@10687
   137
text {*
wenzelm@10687
   138
  The \emph{linear closure} of a vector @{text x} is the set of all
wenzelm@10687
   139
  scalar multiples of @{text x}.
wenzelm@10687
   140
*}
wenzelm@7535
   141
wenzelm@7535
   142
constdefs
wenzelm@10687
   143
  lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
wenzelm@10687
   144
  "lin x \<equiv> {a \<cdot> x | a. True}"
wenzelm@7535
   145
bauerg@9374
   146
lemma linD: "x \<in> lin v = (\<exists>a::real. x = a \<cdot> v)"
wenzelm@9035
   147
  by (unfold lin_def) fast
wenzelm@7535
   148
wenzelm@9408
   149
lemma linI [intro?]: "a \<cdot> x0 \<in> lin x0"
wenzelm@9035
   150
  by (unfold lin_def) fast
wenzelm@7656
   151
wenzelm@9035
   152
text {* Every vector is contained in its linear closure. *}
wenzelm@7917
   153
wenzelm@10687
   154
lemma x_lin_x: "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<in> lin x"
wenzelm@9035
   155
proof (unfold lin_def, intro CollectI exI conjI)
wenzelm@10687
   156
  assume "is_vectorspace V"  "x \<in> V"
bauerg@9374
   157
  show "x = #1 \<cdot> x" by (simp!)
wenzelm@9035
   158
qed simp
wenzelm@7535
   159
wenzelm@9035
   160
text {* Any linear closure is a subspace. *}
wenzelm@7917
   161
wenzelm@10687
   162
lemma lin_subspace [intro?]:
wenzelm@10687
   163
  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_subspace (lin x) V"
wenzelm@9035
   164
proof
wenzelm@10687
   165
  assume "is_vectorspace V"  "x \<in> V"
wenzelm@10687
   166
  show "0 \<in> lin x"
wenzelm@9035
   167
  proof (unfold lin_def, intro CollectI exI conjI)
bauerg@9374
   168
    show "0 = (#0::real) \<cdot> x" by (simp!)
wenzelm@9035
   169
  qed simp
wenzelm@7566
   170
wenzelm@10687
   171
  show "lin x \<subseteq> V"
wenzelm@10687
   172
  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE)
wenzelm@10687
   173
    fix xa a assume "xa = a \<cdot> x"
bauerg@9374
   174
    show "xa \<in> V" by (simp!)
wenzelm@9035
   175
  qed
wenzelm@7566
   176
wenzelm@10687
   177
  show "\<forall>x1 \<in> lin x. \<forall>x2 \<in> lin x. x1 + x2 \<in> lin x"
wenzelm@9035
   178
  proof (intro ballI)
wenzelm@10687
   179
    fix x1 x2 assume "x1 \<in> lin x"  "x2 \<in> lin x"
bauerg@9374
   180
    thus "x1 + x2 \<in> lin x"
wenzelm@10687
   181
    proof (unfold lin_def, elim CollectE exE conjE,
wenzelm@9035
   182
      intro CollectI exI conjI)
wenzelm@10687
   183
      fix a1 a2 assume "x1 = a1 \<cdot> x"  "x2 = a2 \<cdot> x"
wenzelm@10687
   184
      show "x1 + x2 = (a1 + a2) \<cdot> x"
wenzelm@9035
   185
        by (simp! add: vs_add_mult_distrib2)
wenzelm@9035
   186
    qed simp
wenzelm@9035
   187
  qed
wenzelm@7566
   188
wenzelm@10687
   189
  show "\<forall>xa \<in> lin x. \<forall>a. a \<cdot> xa \<in> lin x"
wenzelm@9035
   190
  proof (intro ballI allI)
wenzelm@10687
   191
    fix x1 a assume "x1 \<in> lin x"
bauerg@9374
   192
    thus "a \<cdot> x1 \<in> lin x"
wenzelm@7978
   193
    proof (unfold lin_def, elim CollectE exE conjE,
wenzelm@9035
   194
      intro CollectI exI conjI)
bauerg@9374
   195
      fix a1 assume "x1 = a1 \<cdot> x"
bauerg@9374
   196
      show "a \<cdot> x1 = (a * a1) \<cdot> x" by (simp!)
wenzelm@9035
   197
    qed simp
wenzelm@10687
   198
  qed
wenzelm@9035
   199
qed
wenzelm@7535
   200
wenzelm@9035
   201
text {* Any linear closure is a vector space. *}
wenzelm@7917
   202
wenzelm@10687
   203
lemma lin_vs [intro?]:
wenzelm@10687
   204
  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace (lin x)"
wenzelm@9035
   205
proof (rule subspace_vs)
wenzelm@10687
   206
  assume "is_vectorspace V"  "x \<in> V"
wenzelm@9035
   207
  show "is_subspace (lin x) V" ..
wenzelm@9035
   208
qed
wenzelm@7535
   209
wenzelm@7808
   210
wenzelm@7808
   211
wenzelm@9035
   212
subsection {* Sum of two vectorspaces *}
wenzelm@7808
   213
wenzelm@10687
   214
text {*
wenzelm@10687
   215
  The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
wenzelm@10687
   216
  set of all sums of elements from @{text U} and @{text V}.
wenzelm@10687
   217
*}
wenzelm@7535
   218
wenzelm@10309
   219
instance set :: (plus) plus ..
wenzelm@7917
   220
wenzelm@10687
   221
defs (overloaded)
wenzelm@10687
   222
  vs_sum_def: "U + V \<equiv> {u + v | u v. u \<in> U \<and> v \<in> V}"
wenzelm@7917
   223
wenzelm@10687
   224
lemma vs_sumD:
bauerg@9374
   225
  "x \<in> U + V = (\<exists>u \<in> U. \<exists>v \<in> V. x = u + v)"
wenzelm@9035
   226
    by (unfold vs_sum_def) fast
wenzelm@7535
   227
wenzelm@9941
   228
lemmas vs_sumE = vs_sumD [THEN iffD1, elim_format, standard]
wenzelm@7566
   229
wenzelm@10687
   230
lemma vs_sumI [intro?]:
wenzelm@10687
   231
  "x \<in> U \<Longrightarrow> y \<in> V \<Longrightarrow> t = x + y \<Longrightarrow> t \<in> U + V"
wenzelm@9035
   232
  by (unfold vs_sum_def) fast
wenzelm@7917
   233
wenzelm@10687
   234
text {* @{text U} is a subspace of @{text "U + V"}. *}
wenzelm@7535
   235
wenzelm@10687
   236
lemma subspace_vs_sum1 [intro?]:
wenzelm@10687
   237
  "is_vectorspace U \<Longrightarrow> is_vectorspace V
wenzelm@10687
   238
  \<Longrightarrow> is_subspace U (U + V)"
wenzelm@10687
   239
proof
wenzelm@10687
   240
  assume "is_vectorspace U"  "is_vectorspace V"
bauerg@9374
   241
  show "0 \<in> U" ..
wenzelm@10687
   242
  show "U \<subseteq> U + V"
wenzelm@9035
   243
  proof (intro subsetI vs_sumI)
bauerg@9374
   244
  fix x assume "x \<in> U"
bauerg@9374
   245
    show "x = x + 0" by (simp!)
bauerg@9374
   246
    show "0 \<in> V" by (simp!)
wenzelm@9035
   247
  qed
wenzelm@10687
   248
  show "\<forall>x \<in> U. \<forall>y \<in> U. x + y \<in> U"
wenzelm@9035
   249
  proof (intro ballI)
wenzelm@10687
   250
    fix x y assume "x \<in> U"  "y \<in> U" show "x + y \<in> U" by (simp!)
wenzelm@9035
   251
  qed
wenzelm@10687
   252
  show "\<forall>x \<in> U. \<forall>a. a \<cdot> x \<in> U"
wenzelm@9035
   253
  proof (intro ballI allI)
bauerg@9374
   254
    fix x a assume "x \<in> U" show "a \<cdot> x \<in> U" by (simp!)
wenzelm@9035
   255
  qed
wenzelm@9035
   256
qed
wenzelm@7535
   257
wenzelm@9035
   258
text{* The sum of two subspaces is again a subspace.*}
wenzelm@7917
   259
wenzelm@10687
   260
lemma vs_sum_subspace [intro?]:
wenzelm@10687
   261
  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
wenzelm@10687
   262
  \<Longrightarrow> is_subspace (U + V) E"
wenzelm@10687
   263
proof
wenzelm@10687
   264
  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
bauerg@9374
   265
  show "0 \<in> U + V"
wenzelm@9035
   266
  proof (intro vs_sumI)
bauerg@9374
   267
    show "0 \<in> U" ..
bauerg@9374
   268
    show "0 \<in> V" ..
bauerg@9374
   269
    show "(0::'a) = 0 + 0" by (simp!)
wenzelm@9035
   270
  qed
wenzelm@10687
   271
wenzelm@10687
   272
  show "U + V \<subseteq> E"
wenzelm@9035
   273
  proof (intro subsetI, elim vs_sumE bexE)
wenzelm@10687
   274
    fix x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
bauerg@9374
   275
    show "x \<in> E" by (simp!)
wenzelm@9035
   276
  qed
wenzelm@10687
   277
bauerg@9374
   278
  show "\<forall>x \<in> U + V. \<forall>y \<in> U + V. x + y \<in> U + V"
wenzelm@9035
   279
  proof (intro ballI)
wenzelm@10687
   280
    fix x y assume "x \<in> U + V"  "y \<in> U + V"
bauerg@9374
   281
    thus "x + y \<in> U + V"
wenzelm@9035
   282
    proof (elim vs_sumE bexE, intro vs_sumI)
wenzelm@10687
   283
      fix ux vx uy vy
wenzelm@10687
   284
      assume "ux \<in> U"  "vx \<in> V"  "x = ux + vx"
wenzelm@10687
   285
        and "uy \<in> U"  "vy \<in> V"  "y = uy + vy"
wenzelm@9035
   286
      show "x + y = (ux + uy) + (vx + vy)" by (simp!)
wenzelm@10687
   287
    qed (simp_all!)
wenzelm@9035
   288
  qed
wenzelm@7535
   289
bauerg@9374
   290
  show "\<forall>x \<in> U + V. \<forall>a. a \<cdot> x \<in> U + V"
wenzelm@9035
   291
  proof (intro ballI allI)
bauerg@9374
   292
    fix x a assume "x \<in> U + V"
bauerg@9374
   293
    thus "a \<cdot> x \<in> U + V"
wenzelm@9035
   294
    proof (elim vs_sumE bexE, intro vs_sumI)
wenzelm@10687
   295
      fix a x u v assume "u \<in> U"  "v \<in> V"  "x = u + v"
wenzelm@10687
   296
      show "a \<cdot> x = (a \<cdot> u) + (a \<cdot> v)"
wenzelm@9035
   297
        by (simp! add: vs_add_mult_distrib1)
wenzelm@10687
   298
    qed (simp_all!)
wenzelm@9035
   299
  qed
wenzelm@9035
   300
qed
wenzelm@7535
   301
wenzelm@9035
   302
text{* The sum of two subspaces is a vectorspace. *}
wenzelm@7917
   303
wenzelm@10687
   304
lemma vs_sum_vs [intro?]:
wenzelm@10687
   305
  "is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow> is_vectorspace E
wenzelm@10687
   306
  \<Longrightarrow> is_vectorspace (U + V)"
wenzelm@9035
   307
proof (rule subspace_vs)
wenzelm@10687
   308
  assume "is_subspace U E"  "is_subspace V E"  "is_vectorspace E"
wenzelm@9035
   309
  show "is_subspace (U + V) E" ..
wenzelm@9035
   310
qed
wenzelm@7535
   311
wenzelm@7535
   312
wenzelm@7808
   313
wenzelm@9035
   314
subsection {* Direct sums *}
wenzelm@7808
   315
wenzelm@7535
   316
wenzelm@10687
   317
text {*
wenzelm@10687
   318
  The sum of @{text U} and @{text V} is called \emph{direct}, iff the
wenzelm@10687
   319
  zero element is the only common element of @{text U} and @{text
wenzelm@10687
   320
  V}. For every element @{text x} of the direct sum of @{text U} and
wenzelm@10687
   321
  @{text V} the decomposition in @{text "x = u + v"} with
wenzelm@10687
   322
  @{text "u \<in> U"} and @{text "v \<in> V"} is unique.
wenzelm@10687
   323
*}
wenzelm@7808
   324
wenzelm@10687
   325
lemma decomp:
wenzelm@10687
   326
  "is_vectorspace E \<Longrightarrow> is_subspace U E \<Longrightarrow> is_subspace V E \<Longrightarrow>
wenzelm@10687
   327
  U \<inter> V = {0} \<Longrightarrow> u1 \<in> U \<Longrightarrow> u2 \<in> U \<Longrightarrow> v1 \<in> V \<Longrightarrow> v2 \<in> V \<Longrightarrow>
wenzelm@10687
   328
  u1 + v1 = u2 + v2 \<Longrightarrow> u1 = u2 \<and> v1 = v2"
wenzelm@10687
   329
proof
wenzelm@10687
   330
  assume "is_vectorspace E"  "is_subspace U E"  "is_subspace V E"
wenzelm@10687
   331
    "U \<inter> V = {0}"  "u1 \<in> U"  "u2 \<in> U"  "v1 \<in> V"  "v2 \<in> V"
wenzelm@10687
   332
    "u1 + v1 = u2 + v2"
wenzelm@9035
   333
  have eq: "u1 - u2 = v2 - v1" by (simp! add: vs_add_diff_swap)
wenzelm@10687
   334
  have u: "u1 - u2 \<in> U" by (simp!)
wenzelm@10687
   335
  with eq have v': "v2 - v1 \<in> U" by simp
wenzelm@10687
   336
  have v: "v2 - v1 \<in> V" by (simp!)
bauerg@9374
   337
  with eq have u': "u1 - u2 \<in> V" by simp
wenzelm@10687
   338
wenzelm@9035
   339
  show "u1 = u2"
wenzelm@9035
   340
  proof (rule vs_add_minus_eq)
wenzelm@10687
   341
    show "u1 - u2 = 0" by (rule Int_singletonD [OF _ u u'])
bauerg@9374
   342
    show "u1 \<in> E" ..
bauerg@9374
   343
    show "u2 \<in> E" ..
wenzelm@9035
   344
  qed
wenzelm@7656
   345
wenzelm@9035
   346
  show "v1 = v2"
wenzelm@9623
   347
  proof (rule vs_add_minus_eq [symmetric])
bauerg@9374
   348
    show "v2 - v1 = 0" by (rule Int_singletonD [OF _ v' v])
bauerg@9374
   349
    show "v1 \<in> E" ..
bauerg@9374
   350
    show "v2 \<in> E" ..
wenzelm@9035
   351
  qed
wenzelm@9035
   352
qed
wenzelm@7656
   353
wenzelm@10687
   354
text {*
wenzelm@10687
   355
  An application of the previous lemma will be used in the proof of
wenzelm@10687
   356
  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
wenzelm@10687
   357
  element @{text "y + a \<cdot> x\<^sub>0"} of the direct sum of a
wenzelm@10687
   358
  vectorspace @{text H} and the linear closure of @{text "x\<^sub>0"}
wenzelm@10687
   359
  the components @{text "y \<in> H"} and @{text a} are uniquely
wenzelm@10687
   360
  determined.
wenzelm@10687
   361
*}
wenzelm@7917
   362
wenzelm@10687
   363
lemma decomp_H':
wenzelm@10687
   364
  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> y1 \<in> H \<Longrightarrow> y2 \<in> H \<Longrightarrow>
wenzelm@10687
   365
  x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0 \<Longrightarrow> y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'
wenzelm@10687
   366
  \<Longrightarrow> y1 = y2 \<and> a1 = a2"
wenzelm@9035
   367
proof
wenzelm@7656
   368
  assume "is_vectorspace E" and h: "is_subspace H E"
wenzelm@10687
   369
     and "y1 \<in> H"  "y2 \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
bauerg@9374
   370
         "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
wenzelm@7535
   371
bauerg@9374
   372
  have c: "y1 = y2 \<and> a1 \<cdot> x' = a2 \<cdot> x'"
wenzelm@10687
   373
  proof (rule decomp)
wenzelm@10687
   374
    show "a1 \<cdot> x' \<in> lin x'" ..
bauerg@9374
   375
    show "a2 \<cdot> x' \<in> lin x'" ..
wenzelm@10687
   376
    show "H \<inter> (lin x') = {0}"
wenzelm@9035
   377
    proof
wenzelm@10687
   378
      show "H \<inter> lin x' \<subseteq> {0}"
wenzelm@9623
   379
      proof (intro subsetI, elim IntE, rule singleton_iff [THEN iffD2])
wenzelm@10687
   380
        fix x assume "x \<in> H"  "x \<in> lin x'"
bauerg@9374
   381
        thus "x = 0"
wenzelm@9035
   382
        proof (unfold lin_def, elim CollectE exE conjE)
bauerg@9374
   383
          fix a assume "x = a \<cdot> x'"
wenzelm@9035
   384
          show ?thesis
wenzelm@9035
   385
          proof cases
wenzelm@9035
   386
            assume "a = (#0::real)" show ?thesis by (simp!)
wenzelm@9035
   387
          next
wenzelm@10687
   388
            assume "a \<noteq> (#0::real)"
wenzelm@10687
   389
            from h have "inverse a \<cdot> a \<cdot> x' \<in> H"
wenzelm@9035
   390
              by (rule subspace_mult_closed) (simp!)
bauerg@10606
   391
            also have "inverse a \<cdot> a \<cdot> x' = x'" by (simp!)
bauerg@9374
   392
            finally have "x' \<in> H" .
wenzelm@9035
   393
            thus ?thesis by contradiction
wenzelm@9035
   394
          qed
wenzelm@9035
   395
       qed
wenzelm@9035
   396
      qed
wenzelm@10687
   397
      show "{0} \<subseteq> H \<inter> lin x'"
wenzelm@9035
   398
      proof -
wenzelm@10687
   399
        have "0 \<in> H \<inter> lin x'"
wenzelm@10687
   400
        proof (rule IntI)
wenzelm@10687
   401
          show "0 \<in> H" ..
wenzelm@10687
   402
          from lin_vs show "0 \<in> lin x'" ..
wenzelm@10687
   403
        qed
wenzelm@10687
   404
        thus ?thesis by simp
wenzelm@9035
   405
      qed
wenzelm@9035
   406
    qed
bauerg@9374
   407
    show "is_subspace (lin x') E" ..
wenzelm@9035
   408
  qed
wenzelm@10687
   409
wenzelm@9035
   410
  from c show "y1 = y2" by simp
wenzelm@10687
   411
wenzelm@10687
   412
  show  "a1 = a2"
wenzelm@9623
   413
  proof (rule vs_mult_right_cancel [THEN iffD1])
bauerg@9374
   414
    from c show "a1 \<cdot> x' = a2 \<cdot> x'" by simp
wenzelm@9035
   415
  qed
wenzelm@9035
   416
qed
wenzelm@7535
   417
wenzelm@10687
   418
text {*
wenzelm@10687
   419
  Since for any element @{text "y + a \<cdot> x'"} of the direct sum of a
wenzelm@10687
   420
  vectorspace @{text H} and the linear closure of @{text x'} the
wenzelm@10687
   421
  components @{text "y \<in> H"} and @{text a} are unique, it follows from
wenzelm@10687
   422
  @{text "y \<in> H"} that @{text "a = 0"}.
wenzelm@10687
   423
*}
wenzelm@7917
   424
wenzelm@10687
   425
lemma decomp_H'_H:
wenzelm@10687
   426
  "is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow> t \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E
wenzelm@10687
   427
  \<Longrightarrow> x' \<noteq> 0
wenzelm@10687
   428
  \<Longrightarrow> (SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, (#0::real))"
wenzelm@9370
   429
proof (rule, unfold split_tupled_all)
wenzelm@10687
   430
  assume "is_vectorspace E"  "is_subspace H E"  "t \<in> H"  "x' \<notin> H"  "x' \<in> E"
bauerg@9374
   431
    "x' \<noteq> 0"
wenzelm@9035
   432
  have h: "is_vectorspace H" ..
bauerg@9374
   433
  fix y a presume t1: "t = y + a \<cdot> x'" and "y \<in> H"
wenzelm@10687
   434
  have "y = t \<and> a = (#0::real)"
wenzelm@10687
   435
    by (rule decomp_H') (auto!)
wenzelm@9035
   436
  thus "(y, a) = (t, (#0::real))" by (simp!)
wenzelm@10687
   437
qed (simp_all!)
wenzelm@7535
   438
wenzelm@10687
   439
text {*
wenzelm@10687
   440
  The components @{text "y \<in> H"} and @{text a} in @{text "y + a \<cdot> x'"}
wenzelm@10687
   441
  are unique, so the function @{text h'} defined by
wenzelm@10687
   442
  @{text "h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>"} is definite.
wenzelm@10687
   443
*}
wenzelm@7917
   444
bauerg@9374
   445
lemma h'_definite:
wenzelm@10687
   446
  "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
wenzelm@10687
   447
                in (h y) + a * xi) \<Longrightarrow>
wenzelm@10687
   448
  x = y + a \<cdot> x' \<Longrightarrow> is_vectorspace E \<Longrightarrow> is_subspace H E \<Longrightarrow>
wenzelm@10687
   449
  y \<in> H \<Longrightarrow> x' \<notin> H \<Longrightarrow> x' \<in> E \<Longrightarrow> x' \<noteq> 0
wenzelm@10687
   450
  \<Longrightarrow> h' x = h y + a * xi"
wenzelm@10687
   451
proof -
wenzelm@10687
   452
  assume
wenzelm@10687
   453
    "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
wenzelm@7917
   454
               in (h y) + a * xi)"
wenzelm@10687
   455
    "x = y + a \<cdot> x'"  "is_vectorspace E"  "is_subspace H E"
wenzelm@10687
   456
    "y \<in> H"  "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
wenzelm@10687
   457
  hence "x \<in> H + (lin x')"
wenzelm@10687
   458
    by (auto simp add: vs_sum_def lin_def)
wenzelm@10687
   459
  have "\<exists>! xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
wenzelm@9035
   460
  proof
bauerg@9374
   461
    show "\<exists>xa. ((\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) xa)"
wenzelm@10687
   462
      by (blast!)
wenzelm@9035
   463
  next
wenzelm@9035
   464
    fix xa ya
bauerg@9374
   465
    assume "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) xa"
bauerg@9374
   466
           "(\<lambda>(y,a). x = y + a \<cdot> x' \<and> y \<in> H) ya"
wenzelm@10687
   467
    show "xa = ya"
wenzelm@9035
   468
    proof -
wenzelm@10687
   469
      show "fst xa = fst ya \<and> snd xa = snd ya \<Longrightarrow> xa = ya"
wenzelm@9370
   470
        by (simp add: Pair_fst_snd_eq)
wenzelm@10687
   471
      have x: "x = fst xa + snd xa \<cdot> x' \<and> fst xa \<in> H"
wenzelm@10687
   472
        by (auto!)
wenzelm@10687
   473
      have y: "x = fst ya + snd ya \<cdot> x' \<and> fst ya \<in> H"
wenzelm@10687
   474
        by (auto!)
wenzelm@10687
   475
      from x y show "fst xa = fst ya \<and> snd xa = snd ya"
bauerg@9374
   476
        by (elim conjE) (rule decomp_H', (simp!)+)
wenzelm@9035
   477
    qed
wenzelm@9035
   478
  qed
wenzelm@10687
   479
  hence eq: "(SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H) = (y, a)"
wenzelm@10687
   480
    by (rule some1_equality) (blast!)
bauerg@9374
   481
  thus "h' x = h y + a * xi" by (simp! add: Let_def)
wenzelm@9035
   482
qed
wenzelm@7535
   483
wenzelm@10687
   484
end