relaxed assumptions for dim_image_eq and dim_image_le
authorimmler
Fri Jul 13 12:14:26 2018 +0200 (2 months ago)
changeset 68620707437105595
parent 68619 79abf4201e8d
child 68622 0987ae51a3be
relaxed assumptions for dim_image_eq and dim_image_le
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
src/HOL/Vector_Spaces.thy
     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.4    for S1:: "'b::ab_group_add set" and S2::"'c::ab_group_add set"
     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.57  lemmas_with [var_simplified explicit_ab_group_add,
    2.58      unoverload_type 'e 'b,
    2.59    OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_vector_space_pair_on_with,
    2.60 +  folded lt1.dim_S_def lt2.dim_S_def,
    2.61    untransferred,
    2.62    var_simplified implicit_ab_group_add]:
    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.90 +lemmas_with [var_simplified explicit_ab_group_add,
    2.91 +    unoverload_type 'e 'b,
    2.92 +  OF lt2.type.ab_group_add_axioms lt1.type.ab_group_add_axioms type_finite_dimensional_vector_space_pair_1_on_with,
    2.93 +  folded lt1.dim_S_def lt2.dim_S_def,
    2.94 +  untransferred,
    2.95 +  var_simplified implicit_ab_group_add]:
    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.19 +lemma finite_dimensional_vector_space_pair_1_with[explicit_ab_group_add]:
    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.26  lemma finite_dimensional_vector_space_pair_with[explicit_ab_group_add]:
    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.33 +lemma finite_dimensional_vector_space_pair_1_with_imp_with[explicit_ab_group_add]:
    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.42  lemma finite_dimensional_vector_space_pair_with_imp_finite_dimensional_vector_space_with[explicit_ab_group_add]:
    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.53 -lemma finite_dimensional_vector_space_pair_with_imp_vector_space_with[explicit_ab_group_add]:
    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.150      by (simp add: vs1.finiteI_independent)
   4.151    from C have fC: "finite C"
   4.152      by (simp add: vs2.finiteI_independent)
   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