author immler Fri Jul 13 12:14:26 2018 +0200 (3 days ago) changeset 68620 707437105595 parent 68619 79abf4201e8d child 68622 0987ae51a3be
relaxed assumptions for dim_image_eq and dim_image_le
```     1.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Jul 12 17:23:38 2018 +0100
1.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Fri Jul 13 12:14:26 2018 +0200
1.3 @@ -341,6 +341,11 @@
1.4        intro!: finite_dimensional_vector_space.dimension_def
1.5        finite_dimensional_vector_space_euclidean)
1.6
1.7 +interpretation eucl?: finite_dimensional_vector_space_pair_1
1.8 +  "scaleR::real\<Rightarrow>'a::euclidean_space\<Rightarrow>'a" Basis
1.9 +  "scaleR::real\<Rightarrow>'b::real_vector \<Rightarrow> 'b"
1.10 +  by unfold_locales
1.11 +
1.12  interpretation eucl?: finite_dimensional_vector_space_prod scaleR scaleR Basis Basis
1.13    rewrites "Basis_pair = Basis"
1.14      and "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = (scaleR::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
```
```     2.1 --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Thu Jul 12 17:23:38 2018 +0100
2.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy	Fri Jul 13 12:14:26 2018 +0200
2.3 @@ -142,6 +142,14 @@
2.5      and scale1::"'a::field \<Rightarrow> _" and scale2::"'a \<Rightarrow> _"
2.6
2.7 +locale finite_dimensional_vector_space_pair_1_on =
2.8 +  vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
2.9 +  vs2: vector_space_on S2 scale2
2.10 +  for S1 S2
2.11 +    and scale1::"'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b"
2.12 +    and scale2::"'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c"
2.13 +    and Basis1
2.14 +
2.15  locale finite_dimensional_vector_space_pair_on =
2.16    vs1: finite_dimensional_vector_space_on S1 scale1 Basis1 +
2.17    vs2: finite_dimensional_vector_space_on S2 scale2 Basis2
2.18 @@ -489,6 +497,24 @@
2.19    lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
2.20    by (simp add: type_module_pair_on_with vector_space_pair_on_with_def)
2.21
2.22 +sublocale lt1: local_typedef_vector_space_on S1 scale1 s by unfold_locales
2.23 +sublocale lt2: local_typedef_vector_space_on S2 scale2 t by unfold_locales
2.24 +
2.25 +end
2.26 +
2.27 +locale local_typedef_finite_dimensional_vector_space_pair_1 =
2.28 +  lt1: local_typedef_finite_dimensional_vector_space_on S1 scale1 Basis1 s +
2.29 +  lt2: local_typedef_vector_space_on S2 scale2 t
2.30 +  for S1::"'b::ab_group_add set" and scale1::"'a::field \<Rightarrow> 'b \<Rightarrow> 'b" and Basis1 and s::"'s itself"
2.31 +    and S2::"'c::ab_group_add set" and scale2::"'a \<Rightarrow> 'c \<Rightarrow> 'c" and t::"'t itself"
2.32 +begin
2.33 +
2.34 +lemma type_finite_dimensional_vector_space_pair_1_on_with:
2.35 +  "finite_dimensional_vector_space_pair_1_on_with UNIV UNIV lt1.plus_S lt1.minus_S lt1.uminus_S (lt1.zero_S::'s) lt1.scale_S lt1.Basis_S
2.36 +  lt2.plus_S lt2.minus_S lt2.uminus_S (lt2.zero_S::'t) lt2.scale_S"
2.37 +  by (simp add: finite_dimensional_vector_space_pair_1_on_with_def
2.38 +      lt1.type_finite_dimensional_vector_space_on_with lt2.type_vector_space_on_with)
2.39 +
2.40  end
2.41
2.42  locale local_typedef_finite_dimensional_vector_space_pair =
2.43 @@ -507,6 +533,7 @@
2.44
2.45  end
2.46
2.47 +
2.48  subsection \<open>Transfer from type-based @{theory HOL.Modules} and @{theory HOL.Vector_Spaces}\<close>
2.49
2.50  context module_on begin
2.51 @@ -964,9 +991,12 @@
2.52
2.53  interpretation local_typedef_vector_space_pair S1 scale1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
2.54
2.55 +
2.56 +
2.60 +  folded lt1.dim_S_def lt2.dim_S_def,
2.61    untransferred,
2.63    lt_linear_0 = vector_space_pair.linear_0
2.64 @@ -1007,6 +1037,7 @@
2.65  and lt_linear_injective_left_inverse = vector_space_pair.linear_injective_left_inverse
2.66  and lt_linear_surj_right_inverse = vector_space_pair.linear_surj_right_inverse
2.67  and lt_linear_surjective_right_inverse = vector_space_pair.linear_surjective_right_inverse
2.68 +and lt_finite_basis_to_basis_subspace_isomorphism = vector_space_pair.finite_basis_to_basis_subspace_isomorphism
2.69  (* should work, but doesnt
2.70  *)
2.71  (* not expected to work:
2.72 @@ -1067,9 +1098,42 @@
2.73    and linear_injective_left_inverse = lt_linear_injective_left_inverse
2.74    and linear_surj_right_inverse = lt_linear_surj_right_inverse
2.75    and linear_surjective_right_inverse = lt_linear_surjective_right_inverse
2.76 +  and finite_basis_to_basis_subspace_isomorphism = lt_finite_basis_to_basis_subspace_isomorphism
2.77
2.78  end
2.79
2.80 +context finite_dimensional_vector_space_pair_1_on begin
2.81 +
2.82 +context includes lifting_syntax
2.83 +  notes [transfer_rule del] = Collect_transfer
2.84 +  assumes
2.85 +    "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S1"
2.86 +    "\<exists>(Rep::'t \<Rightarrow> 'c) (Abs::'c \<Rightarrow> 't). type_definition Rep Abs S2" begin
2.87 +
2.88 +interpretation local_typedef_finite_dimensional_vector_space_pair_1 S1 scale1 Basis1 "TYPE('s)" S2 scale2 "TYPE('t)" by unfold_locales fact+
2.89 +
2.93 +  folded lt1.dim_S_def lt2.dim_S_def,
2.94 +  untransferred,
2.96 +   lt_dim_image_eq = finite_dimensional_vector_space_pair_1.dim_image_eq
2.97 +and lt_dim_image_le = finite_dimensional_vector_space_pair_1.dim_image_le
2.98 +
2.99 +end
2.100 +
2.101 +lemmas_with [cancel_type_definition, OF vs1.S_ne,
2.102 +    cancel_type_definition, OF vs2.S_ne,
2.103 +    folded subset_iff' top_set_def,
2.104 +    simplified pred_fun_def,
2.105 +    simplified\<comment>\<open>too much?\<close>]:
2.106 +  dim_image_eq = lt_dim_image_eq
2.107 +and dim_image_le = lt_dim_image_le
2.108 +
2.109 +end
2.110 +
2.111 +
2.112  context finite_dimensional_vector_space_pair_on begin
2.113
2.114  context includes lifting_syntax
2.115 @@ -1090,9 +1154,7 @@
2.116  and lt_linear_injective_imp_surjective = finite_dimensional_vector_space_pair.linear_injective_imp_surjective
2.117  and lt_linear_injective_isomorphism = finite_dimensional_vector_space_pair.linear_injective_isomorphism
2.118  and lt_linear_surjective_isomorphism = finite_dimensional_vector_space_pair.linear_surjective_isomorphism
2.119 -and lt_dim_image_eq = finite_dimensional_vector_space_pair.dim_image_eq
2.120  and lt_basis_to_basis_subspace_isomorphism = finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism
2.121 -and lt_dim_image_le = finite_dimensional_vector_space_pair.dim_image_le
2.122  and lt_subspace_isomorphism = finite_dimensional_vector_space_pair.subspace_isomorphism
2.123
2.124  end
2.125 @@ -1106,9 +1168,7 @@
2.126  and linear_injective_imp_surjective = lt_linear_injective_imp_surjective
2.127  and linear_injective_isomorphism = lt_linear_injective_isomorphism
2.128  and linear_surjective_isomorphism = lt_linear_surjective_isomorphism
2.129 -and dim_image_eq = lt_dim_image_eq
2.130  and basis_to_basis_subspace_isomorphism = lt_basis_to_basis_subspace_isomorphism
2.131 -and dim_image_le = lt_dim_image_le
2.132  and subspace_isomorphism = lt_subspace_isomorphism
2.133
2.134  end
```
```     3.1 --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Thu Jul 12 17:23:38 2018 +0100
3.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Fri Jul 13 12:14:26 2018 +0200
3.3 @@ -119,6 +119,11 @@
3.4      \<not> dependent_with pls zero scl basis \<and>
3.5      span_with pls zero scl basis = S"
3.6
3.7 +definition "finite_dimensional_vector_space_pair_1_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b
3.8 +  pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) \<longleftrightarrow>
3.9 +  finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
3.10 +  vector_space_on_with S' pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_)"
3.11 +
3.12  definition "finite_dimensional_vector_space_pair_on_with S S' pls mns um zero (scl::'a::field\<Rightarrow>_) b
3.13    pls' mns' um' zero' (scl'::'a::field\<Rightarrow>_) b' \<longleftrightarrow>
3.14    finite_dimensional_vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_) b \<and>
3.15 @@ -239,6 +244,13 @@
3.16    by (auto simp: module_pair_on_with_def explicit_ab_group_add
3.17        vector_space_pair_on_with_def vector_space_pair_def module_on_with_def vector_space_on_with_def)
3.18
3.20 +  "finite_dimensional_vector_space_pair_1 s1 b1 s2 \<longleftrightarrow>
3.21 +    finite_dimensional_vector_space_pair_1_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2"
3.22 +  by (auto simp: finite_dimensional_vector_space_pair_1_def
3.23 +      finite_dimensional_vector_space_pair_1_on_with_def finite_dimensional_vector_space_on_with
3.24 +      vector_space_on_with)
3.25 +
3.27    "finite_dimensional_vector_space_pair s1 b1 s2 b2 \<longleftrightarrow>
3.28      finite_dimensional_vector_space_pair_on_with UNIV UNIV (+) (-) uminus 0 s1 b1 (+) (-) uminus 0 s2 b2"
3.29 @@ -261,21 +273,24 @@
3.30    using that
3.31    by (auto simp: vector_space_pair_on_with_def module_pair_on_with_def vector_space_on_with_def)
3.32
3.34 +  "vector_space_on_with S (+) (-) uminus 0 s"
3.35 +  "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
3.36 +  "vector_space_on_with T (+) (-) uminus 0 t"
3.37 +  if "finite_dimensional_vector_space_pair_1_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t"
3.38 +  using that
3.39 +  unfolding finite_dimensional_vector_space_pair_1_on_with_def
3.40 +  by (simp_all add: finite_dimensional_vector_space_on_with_def)
3.41 +
3.43 -  "finite_dimensional_vector_space_on_with S (+) (-) uminus 0 s b"
3.44 +  "vector_space_on_with S (+) (-) uminus 0 s"
3.45 +  "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
3.46 +  "vector_space_on_with T (+) (-) uminus 0 t"
3.47    "finite_dimensional_vector_space_on_with T (+) (-) uminus 0 t c"
3.48    if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
3.49    using that
3.50    unfolding finite_dimensional_vector_space_pair_on_with_def
3.51 -  by simp_all
3.52 -
3.54 -  \<comment>\<open>this rule is strange: why is it needed, but not the one with \<open>module_with\<close> as conclusions?\<close>
3.55 -  "vector_space_on_with S (+) (-) uminus 0 s"
3.56 -  "vector_space_on_with T (+) (-) uminus 0 t"
3.57 -  if "finite_dimensional_vector_space_pair_on_with S T (+) (-) uminus 0 s b (+) (-) uminus 0 t c"
3.58 -  using that
3.59 -  by (auto simp: finite_dimensional_vector_space_pair_on_with_def finite_dimensional_vector_space_on_with_def)
3.60 +  by (simp_all add: finite_dimensional_vector_space_on_with_def)
3.61
3.62  lemma finite_dimensional_vector_space_on_with_transfer[transfer_rule]:
3.63    includes lifting_syntax
```
```     4.1 --- a/src/HOL/Vector_Spaces.thy	Thu Jul 12 17:23:38 2018 +0100
4.2 +++ b/src/HOL/Vector_Spaces.thy	Fri Jul 13 12:14:26 2018 +0200
4.3 @@ -954,6 +954,56 @@
4.4    using linear_surj_right_inverse[of f UNIV UNIV]
4.5    by (auto simp: fun_eq_iff)
4.6
4.7 +lemma finite_basis_to_basis_subspace_isomorphism:
4.8 +  assumes s: "vs1.subspace S"
4.9 +    and t: "vs2.subspace T"
4.10 +    and d: "vs1.dim S = vs2.dim T"
4.11 +    and fB: "finite B"
4.12 +    and B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
4.13 +    and fC: "finite C"
4.14 +    and C: "C \<subseteq> T" "vs2.independent C" "T \<subseteq> vs2.span C" "card C = vs2.dim T"
4.15 +  shows "\<exists>f. linear s1 s2 f \<and> f ` B = C \<and> f ` S = T \<and> inj_on f S"
4.16 +proof -
4.17 +  from B(4) C(4) card_le_inj[of B C] d obtain f where
4.18 +    f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto
4.19 +  from linear_independent_extend[OF B(2)] obtain g where
4.20 +    g: "linear s1 s2 g" "\<forall>x \<in> B. g x = f x" by blast
4.21 +  interpret g: linear s1 s2 g by fact
4.22 +  from inj_on_iff_eq_card[OF fB, of f] f(2)
4.23 +  have "card (f ` B) = card B" by simp
4.24 +  with B(4) C(4) have ceq: "card (f ` B) = card C" using d
4.25 +    by simp
4.26 +  have "g ` B = f ` B" using g(2)
4.27 +    by (auto simp add: image_iff)
4.28 +  also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
4.29 +  finally have gBC: "g ` B = C" .
4.30 +  have gi: "inj_on g B" using f(2) g(2)
4.31 +    by (auto simp add: inj_on_def)
4.32 +  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
4.33 +  {
4.34 +    fix x y
4.35 +    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
4.36 +    from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B"
4.37 +      by blast+
4.38 +    from gxy have th0: "g (x - y) = 0"
4.39 +      by (simp add: g.diff)
4.40 +    have th1: "x - y \<in> vs1.span B" using x' y'
4.41 +      by (metis vs1.span_diff)
4.42 +    have "x = y" using g0[OF th1 th0] by simp
4.43 +  }
4.44 +  then have giS: "inj_on g S" unfolding inj_on_def by blast
4.45 +  from vs1.span_subspace[OF B(1,3) s]
4.46 +  have "g ` S = vs2.span (g ` B)"
4.47 +    by (simp add: g.span_image)
4.48 +  also have "\<dots> = vs2.span C"
4.49 +    unfolding gBC ..
4.50 +  also have "\<dots> = T"
4.51 +    using vs2.span_subspace[OF C(1,3) t] .
4.52 +  finally have gS: "g ` S = T" .
4.53 +  from g(1) gS giS gBC show ?thesis
4.54 +    by blast
4.55 +qed
4.56 +
4.57  end
4.58
4.59  lemma surjective_iff_injective_gen:
4.60 @@ -1366,6 +1416,54 @@
4.61
4.62  end
4.63
4.64 +locale finite_dimensional_vector_space_pair_1 =
4.65 +  vs1: finite_dimensional_vector_space s1 B1 + vs2: vector_space s2
4.66 +  for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
4.67 +  and B1 :: "'b set"
4.68 +  and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
4.69 +begin
4.70 +
4.71 +sublocale vector_space_pair s1 s2 by unfold_locales
4.72 +
4.73 +lemma dim_image_eq:
4.74 +  assumes lf: "linear s1 s2 f"
4.75 +    and fi: "inj_on f (vs1.span S)"
4.76 +  shows "vs2.dim (f ` S) = vs1.dim S"
4.77 +proof -
4.78 +  interpret lf: linear by fact
4.79 +  obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
4.80 +    using vs1.basis_exists[of S] by auto
4.81 +  then have "vs1.span S = vs1.span B"
4.82 +    using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
4.83 +  moreover have "card (f ` B) = card B"
4.84 +    using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
4.85 +  moreover have "(f ` B) \<subseteq> (f ` S)"
4.86 +    using B by auto
4.87 +  ultimately show ?thesis
4.88 +    by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span)
4.89 +qed
4.90 +
4.91 +lemma dim_image_le:
4.92 +  assumes lf: "linear s1 s2 f"
4.93 +  shows "vs2.dim (f ` S) \<le> vs1.dim (S)"
4.94 +proof -
4.95 +  from vs1.basis_exists[of S] obtain B where
4.96 +    B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" by blast
4.97 +  from B have fB: "finite B" "card B = vs1.dim S"
4.98 +    using vs1.independent_bound_general by blast+
4.99 +  have "vs2.dim (f ` S) \<le> card (f ` B)"
4.100 +    apply (rule vs2.span_card_ge_dim)
4.101 +    using lf B fB
4.102 +      apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff
4.103 +        linear_iff_module_hom)
4.104 +    done
4.105 +  also have "\<dots> \<le> vs1.dim S"
4.106 +    using card_image_le[OF fB(1)] fB by simp
4.107 +  finally show ?thesis .
4.108 +qed
4.109 +
4.110 +end
4.111 +
4.112  locale finite_dimensional_vector_space_pair =
4.113    vs1: finite_dimensional_vector_space s1 B1 + vs2: finite_dimensional_vector_space s2 B2
4.114    for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
4.115 @@ -1374,7 +1472,7 @@
4.116    and B2 :: "'c set"
4.117  begin
4.118
4.119 -sublocale vector_space_pair s1 s2 by unfold_locales
4.120 +sublocale finite_dimensional_vector_space_pair_1 ..
4.121
4.122  lemma linear_surjective_imp_injective:
4.123    assumes lf: "linear s1 s2 f" and sf: "surj f" and eq: "vs2.dim UNIV = vs1.dim UNIV"
4.124 @@ -1470,24 +1568,6 @@
4.125      done
4.126  qed
4.127
4.128 -lemma dim_image_eq:
4.129 -  assumes lf: "linear s1 s2 f"
4.130 -    and fi: "inj_on f (vs1.span S)"
4.131 -  shows "vs2.dim (f ` S) = vs1.dim S"
4.132 -proof -
4.133 -  interpret lf: linear by fact
4.134 -  obtain B where B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S"
4.135 -    using vs1.basis_exists[of S] by auto
4.136 -  then have "vs1.span S = vs1.span B"
4.137 -    using vs1.span_mono[of B S] vs1.span_mono[of S "vs1.span B"] vs1.span_span[of B] by auto
4.138 -  moreover have "card (f ` B) = card B"
4.139 -    using assms card_image[of f B] subset_inj_on[of f "vs1.span S" B] B vs1.span_superset by auto
4.140 -  moreover have "(f ` B) \<subseteq> (f ` S)"
4.141 -    using B by auto
4.142 -  ultimately show ?thesis
4.143 -    by (metis B(2) B(4) fi lf.dependent_inj_imageD lf.span_image vs2.dim_eq_card_independent vs2.dim_span)
4.144 -qed
4.145 -
4.146  lemma basis_to_basis_subspace_isomorphism:
4.147    assumes s: "vs1.subspace S"
4.148      and t: "vs2.subspace T"
4.149 @@ -1500,63 +1580,7 @@
4.151    from C have fC: "finite C"
4.153 -  from B(4) C(4) card_le_inj[of B C] d obtain f where
4.154 -    f: "f ` B \<subseteq> C" "inj_on f B" using \<open>finite B\<close> \<open>finite C\<close> by auto
4.155 -  from linear_independent_extend[OF B(2)] obtain g where
4.156 -    g: "linear s1 s2 g" "\<forall>x \<in> B. g x = f x" by blast
4.157 -  interpret g: linear s1 s2 g by fact
4.158 -  from inj_on_iff_eq_card[OF fB, of f] f(2)
4.159 -  have "card (f ` B) = card B" by simp
4.160 -  with B(4) C(4) have ceq: "card (f ` B) = card C" using d
4.161 -    by simp
4.162 -  have "g ` B = f ` B" using g(2)
4.163 -    by (auto simp add: image_iff)
4.164 -  also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
4.165 -  finally have gBC: "g ` B = C" .
4.166 -  have gi: "inj_on g B" using f(2) g(2)
4.167 -    by (auto simp add: inj_on_def)
4.168 -  note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
4.169 -  {
4.170 -    fix x y
4.171 -    assume x: "x \<in> S" and y: "y \<in> S" and gxy: "g x = g y"
4.172 -    from B(3) x y have x': "x \<in> vs1.span B" and y': "y \<in> vs1.span B"
4.173 -      by blast+
4.174 -    from gxy have th0: "g (x - y) = 0"
4.175 -      by (simp add: g.diff)
4.176 -    have th1: "x - y \<in> vs1.span B" using x' y'
4.177 -      by (metis vs1.span_diff)
4.178 -    have "x = y" using g0[OF th1 th0] by simp
4.179 -  }
4.180 -  then have giS: "inj_on g S" unfolding inj_on_def by blast
4.181 -  from vs1.span_subspace[OF B(1,3) s]
4.182 -  have "g ` S = vs2.span (g ` B)"
4.183 -    by (simp add: g.span_image)
4.184 -  also have "\<dots> = vs2.span C"
4.185 -    unfolding gBC ..
4.186 -  also have "\<dots> = T"
4.187 -    using vs2.span_subspace[OF C(1,3) t] .
4.188 -  finally have gS: "g ` S = T" .
4.189 -  from g(1) gS giS gBC show ?thesis
4.190 -    by blast
4.191 -qed
4.192 -
4.193 -lemma dim_image_le:
4.194 -  assumes lf: "linear s1 s2 f"
4.195 -  shows "vs2.dim (f ` S) \<le> vs1.dim (S)"
4.196 -proof -
4.197 -  from vs1.basis_exists[of S] obtain B where
4.198 -    B: "B \<subseteq> S" "vs1.independent B" "S \<subseteq> vs1.span B" "card B = vs1.dim S" by blast
4.199 -  from B have fB: "finite B" "card B = vs1.dim S"
4.200 -    using vs1.independent_bound_general by blast+
4.201 -  have "vs2.dim (f ` S) \<le> card (f ` B)"
4.202 -    apply (rule vs2.span_card_ge_dim)
4.203 -    using lf B fB
4.204 -      apply (auto simp add: module_hom.span_image module_hom.spans_image subset_image_iff
4.205 -        linear_iff_module_hom)
4.206 -    done
4.207 -  also have "\<dots> \<le> vs1.dim S"
4.208 -    using card_image_le[OF fB(1)] fB by simp
4.209 -  finally show ?thesis .
4.210 +  from finite_basis_to_basis_subspace_isomorphism[OF s t d fB B fC C] show ?thesis .
4.211  qed
4.212
4.213  end
```