Theory VS_Vector_Spaces

(* Title: Examples/Vector_Spaces/VS_Vector_Spaces.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins
*)
section‹Vector spaces›
theory VS_Vector_Spaces
  imports VS_Modules
begin



subsection‹‹vector_space_with››

locale vector_space_with = ab_group_add plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S
  for plus⇩V⇩S :: "['vs, 'vs] ⇒ 'vs" (infixl ‹+⇩V⇩S› 65)
    and zero⇩V⇩S (‹0⇩V⇩S›)
    and minus⇩V⇩S (infixl ‹-⇩V⇩S› 65)
    and uminus⇩V⇩S (‹-⇩V⇩S _› [81] 80) +
  fixes scale :: "['f::field, 'vs] ⇒ 'vs" (infixr "*s⇩w⇩i⇩t⇩h" 75)
  assumes scale_right_distrib[algebra_simps]: 
    "a *s⇩w⇩i⇩t⇩h (x +⇩V⇩S y) = a *s⇩w⇩i⇩t⇩h x +⇩V⇩S a *s⇩w⇩i⇩t⇩h y"
    and scale_left_distrib[algebra_simps]:
      "(a + b) *s⇩w⇩i⇩t⇩h x = a *s⇩w⇩i⇩t⇩h x +⇩V⇩S b *s⇩w⇩i⇩t⇩h x"
    and scale_scale[simp]: "a *s⇩w⇩i⇩t⇩h (b *s⇩w⇩i⇩t⇩h x) = (a * b) *s⇩w⇩i⇩t⇩h x"
    and scale_one[simp]: "1 *s⇩w⇩i⇩t⇩h x = x"
begin

notation plus⇩V⇩S (infixl ‹+⇩V⇩S› 65)
  and zero⇩V⇩S (‹0⇩V⇩S›)
  and minus⇩V⇩S (infixl ‹-⇩V⇩S› 65)
  and uminus⇩V⇩S (‹-⇩V⇩S _› [81] 80)
  and scale (infixr "*s⇩w⇩i⇩t⇩h" 75)
  
end

lemma vector_space_with_overloaded[ud_with]: 
  "vector_space = vector_space_with (+) 0 (-) uminus"
  unfolding vector_space_def vector_space_with_def vector_space_with_axioms_def
  by (simp add: field_axioms ab_group_add_axioms)

locale vector_space_pair_with =
  VS⇩1: vector_space_with plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_with plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  for plus⇩V⇩S⇩_⇩1 :: "['vs_1, 'vs_1] ⇒ 'vs_1" (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1"  (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
    and plus⇩V⇩S⇩_⇩2 :: "['vs_2, 'vs_2] ⇒ 'vs_2" (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75)

lemma vector_space_pair_with_overloaded[ud_with]: 
  "vector_space_pair = 
    (
      λscale⇩1 scale⇩2. 
        vector_space_pair_with (+) 0 (-) uminus scale⇩1 (+) 0 (-) uminus scale⇩2
    )"
  unfolding vector_space_pair_def vector_space_pair_with_def 
  unfolding vector_space_with_overloaded
  ..

locale linear_with =
  VS⇩1: vector_space_with plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_with plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 +
  module_hom_with 
    plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
    plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
    f 
  for plus⇩V⇩S⇩_⇩1 :: "['vs_1, 'vs_1] ⇒ 'vs_1" (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1"  (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
    and plus⇩V⇩S⇩_⇩2 :: "['vs_2, 'vs_2] ⇒ 'vs_2" (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75)
    and f :: "'vs_1 ⇒ 'vs_2"

lemma linear_with_overloaded[ud_with]: 
  "Vector_Spaces.linear = 
    (
      λscale⇩1 scale⇩2. 
        linear_with (+) 0 (-) uminus scale⇩1 (+) 0 (-) uminus scale⇩2
    )"
  unfolding 
    Vector_Spaces.linear_def linear_with_def 
    vector_space_with_overloaded module_hom_with_overloaded
  ..

locale finite_dimensional_vector_space_with = 
  vector_space_with plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale
  for plus⇩V⇩S :: "['vs, 'vs] ⇒ 'vs"
    and zero⇩V⇩S 
    and minus⇩V⇩S 
    and uminus⇩V⇩S 
    and scale :: "['f::field, 'vs] ⇒ 'vs" +
  fixes basis :: "'vs set"
  assumes finite_basis: "finite basis"
    and independent_basis: "independent_with 0 0⇩V⇩S (+⇩V⇩S) (*s⇩w⇩i⇩t⇩h) basis"
    and span_basis: "span.with 0⇩V⇩S (+⇩V⇩S) (*s⇩w⇩i⇩t⇩h) basis = UNIV"

lemma finite_dimensional_vector_space_with_overloaded[ud_with]: 
  "finite_dimensional_vector_space = 
    finite_dimensional_vector_space_with (+) 0 (-) uminus"
  unfolding
    finite_dimensional_vector_space_def
    finite_dimensional_vector_space_axioms_def
    finite_dimensional_vector_space_with_def
    finite_dimensional_vector_space_with_axioms_def
  by (intro ext)
    (
      auto simp: 
        vector_space_with_overloaded 
        dependent.with 
        module_iff_vector_space
        span.with 
    )

locale finite_dimensional_vector_space_pair_1_with = 
  VS⇩1: finite_dimensional_vector_space_with 
    plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1 +
  VS⇩2: vector_space_with 
    plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  for plus⇩V⇩S⇩_⇩1 :: "['vs_1, 'vs_1] ⇒ 'vs_1" (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
    and basis⇩1
    and plus⇩V⇩S⇩_⇩2 :: "['vs_2, 'vs_2] ⇒ 'vs_2" (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75)

lemma finite_dimensional_vector_space_pair_1_with_overloaded[ud_with]: 
  "finite_dimensional_vector_space_pair_1 = 
    (
      λscale⇩1 basis⇩1 scale⇩2. 
        finite_dimensional_vector_space_pair_1_with 
          (+) 0 (-) uminus scale⇩1 basis⇩1 (+) 0 (-) uminus scale⇩2
    )"
  unfolding
    finite_dimensional_vector_space_pair_1_def
    finite_dimensional_vector_space_pair_1_with_def    
    vector_space_with_overloaded
  by (simp add: finite_dimensional_vector_space_with_overloaded)

locale finite_dimensional_vector_space_pair_with = 
  VS⇩1: finite_dimensional_vector_space_with 
    plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1 +
  VS⇩2: finite_dimensional_vector_space_with 
    plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 basis⇩2
  for plus⇩V⇩S⇩_⇩1 :: "['vs_1, 'vs_1] ⇒ 'vs_1" (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
    and basis⇩1
    and plus⇩V⇩S⇩_⇩2 :: "['vs_2, 'vs_2] ⇒ 'vs_2" (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75)
    and basis⇩2

lemma finite_dimensional_vector_space_pair_with_overloaded[ud_with]: 
  "finite_dimensional_vector_space_pair = 
    (
      λscale⇩1 basis⇩1 scale⇩2 basis⇩2. 
        finite_dimensional_vector_space_pair_with 
          (+) 0 (-) uminus scale⇩1 basis⇩1 (+) 0 (-) uminus scale⇩2 basis⇩2
    )"
  unfolding
    finite_dimensional_vector_space_pair_def
    finite_dimensional_vector_space_pair_with_def
    finite_dimensional_vector_space_with_overloaded
  ..



subsection‹‹vector_space_ow››


subsubsection‹Definitions and common properties›


text‹Single vector space.›

locale vector_space_ow = ab_group_add_ow U⇩V⇩S plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S
  for U⇩V⇩S :: "'vs set" 
    and plus⇩V⇩S (infixl ‹+⇩V⇩S› 65)
    and zero⇩V⇩S (‹0⇩V⇩S›)
    and minus⇩V⇩S (infixl ‹-⇩V⇩S› 65)
    and uminus⇩V⇩S (‹-⇩V⇩S _› [81] 80) +
  fixes scale :: "['f::field, 'vs] ⇒ 'vs" (infixr "*s⇩o⇩w" 75)
  assumes scale_closed[simp, intro]: "x ∈ U⇩V⇩S ⟹ a *s⇩o⇩w x ∈ U⇩V⇩S"
    and scale_right_distrib[algebra_simps]: 
    "⟦ x ∈ U⇩V⇩S; y ∈ U⇩V⇩S ⟧ ⟹ a *s⇩o⇩w (x +⇩V⇩S y) = a *s⇩o⇩w x +⇩V⇩S a *s⇩o⇩w y"
    and scale_left_distrib[algebra_simps]: 
      "x ∈ U⇩V⇩S ⟹ (a + b) *s⇩o⇩w x = a *s⇩o⇩w x +⇩V⇩S b *s⇩o⇩w x"
    and scale_scale[simp]: 
      "x ∈ U⇩V⇩S ⟹ a *s⇩o⇩w (b *s⇩o⇩w x) = (a * b) *s⇩o⇩w x"
    and scale_one[simp]: "x ∈ U⇩V⇩S ⟹ 1 *s⇩o⇩w x = x"
begin

lemma scale_closed'[simp]: "∀a. ∀x∈U⇩V⇩S. a *s⇩o⇩w x ∈ U⇩V⇩S" by simp

lemma minus_closed'[simp]: "∀x∈U⇩V⇩S. ∀y∈U⇩V⇩S. x -⇩V⇩S y ∈ U⇩V⇩S"
  by (simp add: ab_diff_conv_add_uminus add_closed' uminus_closed)

lemma uminus_closed'[simp]: "∀x∈U⇩V⇩S. -⇩V⇩S x ∈ U⇩V⇩S" by (simp add: uminus_closed)

tts_register_sbts ‹(*s⇩o⇩w)› | U⇩V⇩S
  by (rule tts_AB_C_transfer[OF scale_closed]) 
    (auto simp: bi_unique_eq right_total_eq)

sublocale implicit⇩V⇩S: module_ow U⇩V⇩S plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale
  by unfold_locales (simp_all add: scale_right_distrib scale_left_distrib)

end

ud ‹vector_space.dim›
ud dim' ‹dim›


text‹Pair of vector spaces.›

locale vector_space_pair_ow = 
  VS⇩1: vector_space_ow U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_ow U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  for U⇩V⇩S⇩_⇩1 :: "'vs_1 set"
    and plus⇩V⇩S⇩_⇩1 (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩o⇩w⇩'_⇩1› 75)
    and U⇩V⇩S⇩_⇩2 :: "'vs_2 set"
    and plus⇩V⇩S⇩_⇩2 (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩o⇩w⇩'_⇩2› 75)
begin

sublocale implicit⇩V⇩S: module_pair_ow 
  U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
  U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  by unfold_locales

end


text‹Linear map.›

locale linear_ow =
  VS⇩1: vector_space_ow U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_ow U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 +
  module_hom_ow 
    U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
    U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
    f 
  for U⇩V⇩S⇩_⇩1 :: "'vs_1 set"
    and plus⇩V⇩S⇩_⇩1 (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩o⇩w⇩'_⇩1› 75)
    and U⇩V⇩S⇩_⇩2 :: "'vs_2 set"
    and plus⇩V⇩S⇩_⇩2 (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩o⇩w⇩'_⇩2› 75)
    and f :: "'vs_1 ⇒ 'vs_2"
begin

sublocale implicit⇩V⇩S: vector_space_pair_ow
  U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
  U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  by unfold_locales

end


text‹Single finite dimensional vector space.›

locale finite_dimensional_vector_space_ow = 
  vector_space_ow U⇩V⇩S plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale
  for U⇩V⇩S :: "'vs set"
    and plus⇩V⇩S (infixl ‹+⇩V⇩S› 65)
    and zero⇩V⇩S (‹0⇩V⇩S›)
    and minus⇩V⇩S (infixl ‹-⇩V⇩S› 65)
    and uminus⇩V⇩S (‹-⇩V⇩S _› [81] 80) 
    and scale :: "['f::field, 'vs] ⇒ 'vs" (infixr "*s⇩o⇩w" 75) +
  fixes basis :: "'vs set"
  assumes basis_closed: "basis ⊆ U⇩V⇩S"
    and finite_basis: "finite basis"
    and independent_basis: "independent_with 0 zero⇩V⇩S plus⇩V⇩S scale basis"
    and span_basis: "span.with zero⇩V⇩S plus⇩V⇩S scale basis = U⇩V⇩S"


text‹Pair of finite dimensional vector spaces.›

locale finite_dimensional_vector_space_pair_1_ow =
  VS⇩1: finite_dimensional_vector_space_ow
    U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1 +
  VS⇩2: vector_space_ow 
    U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
  for U⇩V⇩S⇩_⇩1 :: "'vs_1 set"
    and plus⇩V⇩S⇩_⇩1 (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩o⇩w⇩'_⇩1› 75)
    and basis⇩1
    and U⇩V⇩S⇩_⇩2 :: "'vs_2 set"
    and plus⇩V⇩S⇩_⇩2 (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩o⇩w⇩'_⇩2› 75)

locale finite_dimensional_vector_space_pair_ow = 
  VS⇩1: finite_dimensional_vector_space_ow 
    U⇩V⇩S⇩_⇩1 plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1 + 
  VS⇩2: finite_dimensional_vector_space_ow 
    U⇩V⇩S⇩_⇩2 plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 basis⇩2
  for U⇩V⇩S⇩_⇩1 :: "'vs_1 set"
    and plus⇩V⇩S⇩_⇩1 (infixl ‹+⇩V⇩S⇩'_⇩1› 65)
    and zero⇩V⇩S⇩_⇩1 (‹0⇩V⇩S⇩'_⇩1›)
    and minus⇩V⇩S⇩_⇩1 (infixl ‹-⇩V⇩S⇩'_⇩1› 65)
    and uminus⇩V⇩S⇩_⇩1 (‹-⇩V⇩S⇩'_⇩1 _› [81] 80)
    and scale⇩1 :: "['f::field, 'vs_1] ⇒ 'vs_1" (infixr ‹*s⇩o⇩w⇩'_⇩1› 75)
    and basis⇩1
    and U⇩V⇩S⇩_⇩2 :: "'vs_2 set"
    and plus⇩V⇩S⇩_⇩2 (infixl ‹+⇩V⇩S⇩'_⇩2› 65)
    and zero⇩V⇩S⇩_⇩2 (‹0⇩V⇩S⇩'_⇩2›)
    and minus⇩V⇩S⇩_⇩2 (infixl ‹-⇩V⇩S⇩'_⇩2› 65)
    and uminus⇩V⇩S⇩_⇩2 (‹-⇩V⇩S⇩'_⇩2 _› [81] 80)
    and scale⇩2 :: "['f::field, 'vs_2] ⇒ 'vs_2" (infixr ‹*s⇩o⇩w⇩'_⇩2› 75)
    and basis⇩2


subsubsection‹Transfer.›

lemma vector_space_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique B" "right_total B"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B ===> B ===> B) ===>
        B ===>
        (B ===> B ===> B) ===>
        (B ===> B) ===>
        ((=) ===> B ===> B) ===>
        (=)
      )"
    and
      "lhs ≡ 
        (
          λplus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale.
            vector_space_ow 
              (Collect (Domainp B)) plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale
        )"
  shows "PP lhs vector_space_with"
proof-
  let ?rhs = 
    "(
      λplus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale.
        (∀a ∈ UNIV. ∀x ∈ UNIV. scale a x ∈ UNIV) ∧
         vector_space_with plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale
    )"
  have "PP lhs ?rhs"
    unfolding 
      PP_def lhs_def
      vector_space_ow_def vector_space_with_def
      vector_space_ow_axioms_def vector_space_with_axioms_def
    apply transfer_prover_start
    apply transfer_step+
    by (intro ext) blast
  then show ?thesis by simp
qed

lemma vector_space_pair_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: 
    "bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        B⇩1 ===>
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        (B⇩1 ===> B⇩1) ===>
        ((=) ===> B⇩1 ===> B⇩1) ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        B⇩2 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        (B⇩2 ===> B⇩2) ===>
        ((=) ===> B⇩2 ===> B⇩2) ===>
        (=)
    )"
    and
      "lhs ≡ 
        (
          λ
            plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2.
          vector_space_pair_ow 
            (Collect (Domainp B⇩1)) plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            (Collect (Domainp B⇩2)) plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
        )"
    shows "PP lhs vector_space_pair_with"
  unfolding PP_def lhs_def
  unfolding vector_space_pair_ow_def vector_space_pair_with_def
  by transfer_prover

lemma linear_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: 
    "bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        B⇩1 ===>
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        (B⇩1 ===> B⇩1) ===>
        ((=) ===> B⇩1 ===> B⇩1) ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        B⇩2 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        (B⇩2 ===> B⇩2) ===>
        ((=) ===> B⇩2 ===> B⇩2) ===>
        (B⇩1 ===> B⇩2) ===>
        (=)
    )"
    and
      "lhs ≡ 
        (
          λ
            plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
            f.
          linear_ow 
            (Collect (Domainp B⇩1)) plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            (Collect (Domainp B⇩2)) plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
            f
        )
      "
    shows "PP lhs linear_with"
  unfolding PP_def lhs_def
  unfolding linear_ow_def linear_with_def
  by transfer_prover

lemma linear_with_transfer'[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique B" "right_total B"
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B ===> B ===> B) ===>
        B ===>
        (B ===> B ===> B) ===>
        (B ===> B) ===>
        ((=) ===> B ===> B) ===>
        (B ===> B ===> B) ===>
        B ===>
        (B ===> B ===> B) ===>
        (B ===> B) ===>
        ((=) ===> B ===> B) ===>
        (B ===> B) ===>
        (=)
    )"
    and
      "lhs ≡ 
        (
          λ
            plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
            f.
          linear_ow 
            (Collect (Domainp B)) plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1
            (Collect (Domainp B)) plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
            f
        )
      "
    shows "PP lhs linear_with"
  unfolding PP_def lhs_def
  using assms(1,2) by (rule linear_with_transfer[OF assms(1,2)])

lemma finite_dimensional_vector_space_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique B" "right_total B"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B ===> B ===> B) ===>
        B ===>
        (B ===> B ===> B) ===>
        (B ===> B) ===>
        ((=) ===> B ===> B) ===>
        rel_set B ===>
        (=)
      )"
    and
      "lhs ≡ 
        (
          λplus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale basis.
            finite_dimensional_vector_space_ow 
              (Collect (Domainp B)) plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale basis
        )"
    shows "PP lhs finite_dimensional_vector_space_with"
proof-
  let ?rhs = 
    "(
      λplus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale basis.
        basis ⊆ UNIV ∧
        finite_dimensional_vector_space_with 
          plus⇩V⇩S zero⇩V⇩S minus⇩V⇩S uminus⇩V⇩S scale basis
    )"
  have "PP lhs ?rhs"
    unfolding 
      PP_def lhs_def
      finite_dimensional_vector_space_ow_def 
      finite_dimensional_vector_space_with_def
      finite_dimensional_vector_space_ow_axioms_def
      finite_dimensional_vector_space_with_axioms_def
    apply transfer_prover_start
    apply transfer_step+
    by blast
  then show ?thesis by simp
qed

lemma finite_dimensional_vector_space_pair_1_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: 
    "bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        B⇩1 ===>
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        (B⇩1 ===> B⇩1) ===>
        ((=) ===> B⇩1 ===> B⇩1) ===>
        rel_set B⇩1 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        B⇩2 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        (B⇩2 ===> B⇩2) ===>
        ((=) ===> B⇩2 ===> B⇩2) ===>
        (=)
    )"
    and
      "lhs ≡ 
        (
          λ
            plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1
            plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2.
          finite_dimensional_vector_space_pair_1_ow 
            (Collect (Domainp B⇩1)) 
              plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1
            (Collect (Domainp B⇩2)) 
              plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2
        )"
    shows "PP lhs finite_dimensional_vector_space_pair_1_with"
  unfolding PP_def lhs_def
  unfolding 
    finite_dimensional_vector_space_pair_1_ow_def
    finite_dimensional_vector_space_pair_1_with_def
  by transfer_prover

lemma finite_dimensional_vector_space_pair_with_transfer[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: 
    "bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"     
  fixes PP lhs
  defines
    "PP ≡ 
      (
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        B⇩1 ===>
        (B⇩1 ===> B⇩1 ===> B⇩1) ===>
        (B⇩1 ===> B⇩1) ===>
        ((=) ===> B⇩1 ===> B⇩1) ===>
        rel_set B⇩1 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        B⇩2 ===>
        (B⇩2 ===> B⇩2 ===> B⇩2) ===>
        (B⇩2 ===> B⇩2) ===>
        ((=) ===> B⇩2 ===> B⇩2) ===>
        rel_set B⇩2 ===>
        (=)
      )"
    and
      "lhs ≡ 
        (
          λ
            plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1
            plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 basis⇩2.
          finite_dimensional_vector_space_pair_ow 
            (Collect (Domainp B⇩1)) 
              plus⇩V⇩S⇩_⇩1 zero⇩V⇩S⇩_⇩1 minus⇩V⇩S⇩_⇩1 uminus⇩V⇩S⇩_⇩1 scale⇩1 basis⇩1
            (Collect (Domainp B⇩2)) 
              plus⇩V⇩S⇩_⇩2 zero⇩V⇩S⇩_⇩2 minus⇩V⇩S⇩_⇩2 uminus⇩V⇩S⇩_⇩2 scale⇩2 basis⇩2
        )"
    shows "PP lhs finite_dimensional_vector_space_pair_with"
  unfolding PP_def lhs_def
  unfolding 
    finite_dimensional_vector_space_pair_ow_def
    finite_dimensional_vector_space_pair_with_def
  by transfer_prover



subsection‹‹vector_space_on››

locale vector_space_on = module_on U⇩V⇩S scale
  for U⇩V⇩S and scale :: "'a::field ⇒ 'b::ab_group_add ⇒ 'b" (infixr "*s" 75)
begin

notation scale (infixr "*s" 75)

sublocale implicit⇩V⇩S: vector_space_ow U⇩V⇩S ‹(+)› 0 ‹(-)› uminus scale
  by unfold_locales 
    (simp_all add: scale_right_distrib_on scale_left_distrib_on)

lemmas ab_group_add_ow_axioms = implicit⇩M.ab_group_add_ow_axioms
lemmas vector_space_ow_axioms = implicit⇩V⇩S.vector_space_ow_axioms

definition dim :: "'b set ⇒ nat"
  where "dim V = (if ∃b⊆U⇩V⇩S. ¬ dependent b ∧ span b = span V
    then card (SOME b. b ⊆ U⇩V⇩S ∧ ¬ dependent b ∧ span b = span V)
    else 0)"

end

lemma vector_space_on_alt_def: "vector_space_on U⇩V⇩S = module_on U⇩V⇩S"
  unfolding vector_space_on_def module_on_def
  by auto

lemma implicit_vector_space_ow[tts_implicit]:
  "vector_space_ow U⇩V⇩S (+) 0 (-) uminus = vector_space_on U⇩V⇩S"
proof(intro ext, rule iffI)
  fix s :: "'a ⇒ 'b ⇒ 'b" 
  assume "vector_space_ow U⇩V⇩S (+) 0 (-) uminus s"
  then interpret vector_space_ow U⇩V⇩S ‹(+)› 0 ‹(-)› uminus s .
  show "vector_space_on U⇩V⇩S s"
    by 
      (
        simp add: 
          scale_left_distrib 
          scale_right_distrib
          module_on_def 
          vector_space_on_def
      )
qed (rule vector_space_on.vector_space_ow_axioms)

locale linear_on = 
  VS⇩1: vector_space_on U⇩M⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_on U⇩M⇩_⇩2 scale⇩2 +
  module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 f
  for U⇩M⇩_⇩1 U⇩M⇩_⇩2 and scale⇩1::"'a::field ⇒ 'b ⇒ 'b::ab_group_add"
    and scale⇩2::"'a::field ⇒ 'c ⇒ 'c::ab_group_add"
    and f

lemma implicit_linear_on[tts_implicit]:
  "linear_ow U⇩M⇩_⇩1 (+) 0 minus uminus scale⇩1 U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 = 
    linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2"
  unfolding linear_ow_def linear_on_def tts_implicit ..

locale finite_dimensional_vector_space_on =
  vector_space_on U⇩V⇩S scale 
  for U⇩V⇩S :: "'b::ab_group_add set" 
    and scale :: "'a::field ⇒ 'b ⇒ 'b" +
  fixes basis :: "'b set"
  assumes finite_basis: "finite basis"
    and independent_basis: "¬ dependent basis"
    and span_basis: "span basis = U⇩V⇩S" 
    and basis_subset: "basis ⊆ U⇩V⇩S"
begin

sublocale implicit⇩V⇩S: 
  finite_dimensional_vector_space_ow U⇩V⇩S ‹(+)› 0 ‹(-)› uminus scale basis
  by unfold_locales 
    (
      simp_all add: 
        finite_basis 
        implicit_dependent_with 
        independent_basis  
        implicit_span_with
        span_basis
        basis_subset
    )

end

lemma implicit_finite_dimensional_vector_space_on[tts_implicit]:
  "finite_dimensional_vector_space_ow U⇩V⇩S (+) 0 minus uminus scale basis = 
    finite_dimensional_vector_space_on U⇩V⇩S scale basis"
  unfolding 
    finite_dimensional_vector_space_ow_def 
    finite_dimensional_vector_space_on_def  
    finite_dimensional_vector_space_ow_axioms_def
    finite_dimensional_vector_space_on_axioms_def  
    vector_space_on_alt_def
    tts_implicit
  by (metis module_on.implicit_dependent_with module_on.implicit_span_with)  

locale vector_space_pair_on = 
  VS⇩1: vector_space_on U⇩M⇩_⇩1 scale⇩1 +
  VS⇩2: vector_space_on U⇩M⇩_⇩2 scale⇩2
  for U⇩M⇩_⇩1:: "'b::ab_group_add set" and U⇩M⇩_⇩2::"'c::ab_group_add set"
    and scale⇩1::"'a::field ⇒ _ ⇒ _" (infixr ‹*s⇩1› 75) 
    and scale⇩2::"'a ⇒ _ ⇒ _" (infixr ‹*s⇩2› 75)
begin

notation scale⇩1 (infixr ‹*s⇩1› 75)
notation scale⇩2 (infixr ‹*s⇩2› 75)

sublocale module_pair_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 by unfold_locales

sublocale implicit⇩V⇩S: 
  vector_space_pair_ow 
    U⇩M⇩_⇩1 ‹(+)› 0 ‹(-)› uminus scale⇩1 
    U⇩M⇩_⇩2 ‹(+)› 0 ‹(-)› uminus scale⇩2
  by unfold_locales

end

lemma implicit_vector_space_pair_on[tts_implicit]:
  "vector_space_pair_ow 
    U⇩M⇩_⇩1 (+) 0 (-) uminus scale⇩1 
    U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 = 
    vector_space_pair_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2"
  unfolding vector_space_pair_ow_def vector_space_pair_on_def tts_implicit ..

locale finite_dimensional_vector_space_pair_1_on =
  VS⇩1: finite_dimensional_vector_space_on U⇩M⇩_⇩1 scale⇩1 basis1 +
  VS⇩2: vector_space_on U⇩M⇩_⇩2 scale⇩2
  for U⇩M⇩_⇩1 U⇩M⇩_⇩2
    and scale⇩1::"'a::field ⇒ 'b::ab_group_add ⇒ 'b"
    and scale⇩2::"'a::field ⇒ 'c::ab_group_add ⇒ 'c"
    and basis1
begin

sublocale vector_space_pair_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 by unfold_locales

sublocale implicit⇩V⇩S:
  finite_dimensional_vector_space_pair_1_ow 
    U⇩M⇩_⇩1 ‹(+)› 0 ‹(-)› uminus scale⇩1 basis1 U⇩M⇩_⇩2 ‹(+)› 0 ‹(-)› uminus scale⇩2
  by unfold_locales

end

lemma implicit_finite_dimensional_vector_space_pair_1_on[tts_implicit]:
  "finite_dimensional_vector_space_pair_1_ow 
    U⇩M⇩_⇩1 (+) 0 minus uminus scale⇩1 basis1 U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 = 
    finite_dimensional_vector_space_pair_1_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 basis1"
  unfolding 
    finite_dimensional_vector_space_pair_1_ow_def 
    finite_dimensional_vector_space_pair_1_on_def 
    tts_implicit 
    ..

locale finite_dimensional_vector_space_pair_on =
  VS⇩1: finite_dimensional_vector_space_on U⇩M⇩_⇩1 scale⇩1 basis1 +
  VS⇩2: finite_dimensional_vector_space_on U⇩M⇩_⇩2 scale⇩2 basis2
  for U⇩M⇩_⇩1 U⇩M⇩_⇩2
    and scale⇩1::"'a::field ⇒ 'b::ab_group_add ⇒ 'b"
    and scale⇩2::"'a::field ⇒ 'c::ab_group_add ⇒ 'c"
    and basis1 basis2
begin

sublocale finite_dimensional_vector_space_pair_1_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 
  by unfold_locales

sublocale implicit⇩V⇩S: 
  finite_dimensional_vector_space_pair_ow 
    U⇩M⇩_⇩1 ‹(+)› 0 ‹(-)› uminus scale⇩1 basis1 
    U⇩M⇩_⇩2 ‹(+)› 0 ‹(-)› uminus scale⇩2 basis2
  by unfold_locales

end

lemma implicit_finite_dimensional_vector_space_pair_on[tts_implicit]:
  "finite_dimensional_vector_space_pair_ow 
      U⇩M⇩_⇩1 (+) 0 minus uminus scale⇩1 basis1 
      U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 basis2 = 
    finite_dimensional_vector_space_pair_on 
      U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 basis1 basis2"
  unfolding 
    finite_dimensional_vector_space_pair_ow_def 
    finite_dimensional_vector_space_pair_on_def 
    tts_implicit 
    ..



subsection‹Relativization : part I›

context vector_space_on
begin

tts_context
  tts: (?'b to ‹U⇩V⇩S::'b set›)
  rewriting ctr_simps
  substituting ab_group_add_ow_axioms
    and vector_space_ow_axioms
    and implicit⇩M.module_ow_axioms
  applying 
    [
      OF 
        implicit⇩M.carrier_ne 
        implicit⇩M.add_closed' 
        implicit⇩M.zero_closed 
        implicit⇩V⇩S.minus_closed' 
        implicit⇩V⇩S.uminus_closed' 
        implicit⇩V⇩S.scale_closed',
      unfolded tts_implicit
    ]
begin

tts_lemma linear_id: "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) id"
  is vector_space.linear_id.

tts_lemma linear_ident: "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) (λx. x)"
  is vector_space.linear_ident.
    
tts_lemma linear_scale_self: "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) ((*s) c)"
  is vector_space.linear_scale_self.
    
tts_lemma linear_scale_left:
  assumes "x ∈ U⇩V⇩S"
  shows "linear_on UNIV U⇩V⇩S (*) (*s) (λr. r *s x)"
    is vector_space.linear_scale_left.
    
tts_lemma linear_uminus: "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) uminus"
    is vector_space.linear_uminus.
    
tts_lemma linear_imp_scale["consumes" - 1, "case_names" "1"]:
  assumes "range D ⊆ U⇩V⇩S"
    and "linear_on UNIV U⇩V⇩S (*) (*s) D"
    and "⋀d. ⟦d ∈ U⇩V⇩S; D = (λx. x *s d)⟧ ⟹ thesis"
  shows thesis
    is vector_space.linear_imp_scale.

tts_lemma scale_eq_0_iff:
  assumes "x ∈ U⇩V⇩S"
  shows "(a *s x = 0) = (a = 0 ∨ x = 0)"
    is vector_space.scale_eq_0_iff.

tts_lemma scale_left_imp_eq:
  assumes "x ∈ U⇩V⇩S" and "y ∈ U⇩V⇩S" and "a ≠ 0" and "a *s x = a *s y"
  shows "x = y"
    is vector_space.scale_left_imp_eq.

tts_lemma scale_right_imp_eq:
  assumes "x ∈ U⇩V⇩S" and "x ≠ 0" and "a *s x = b *s x"
  shows "a = b"
    is vector_space.scale_right_imp_eq.

tts_lemma scale_cancel_left:
  assumes "x ∈ U⇩V⇩S" and "y ∈ U⇩V⇩S"
  shows "(a *s x = a *s y) = (x = y ∨ a = 0)"
    is vector_space.scale_cancel_left.

tts_lemma scale_cancel_right:
  assumes "x ∈ U⇩V⇩S"
  shows "(a *s x = b *s x) = (a = b ∨ x = 0)"
    is vector_space.scale_cancel_right.

tts_lemma injective_scale:
  assumes "c ≠ 0"
  shows "inj_on ((*s) c) U⇩V⇩S"
    is vector_space.injective_scale.

tts_lemma dependent_def:
  assumes "P ⊆ U⇩V⇩S"
  shows "dependent P = (∃x∈P. x ∈ span (P - {x}))"
    is vector_space.dependent_def.

tts_lemma dependent_single:
  assumes "x ∈ U⇩V⇩S"
  shows "dependent {x} = (x = 0)"
    is vector_space.dependent_single.

tts_lemma in_span_insert:
  assumes "a ∈ U⇩V⇩S"
    and "b ∈ U⇩V⇩S"
    and "S ⊆ U⇩V⇩S"
    and "a ∈ span (insert b S)"
    and "a ∉ span S"
  shows "b ∈ span (insert a S)"
    is vector_space.in_span_insert.

tts_lemma dependent_insertD:
  assumes "a ∈ U⇩V⇩S" and "S ⊆ U⇩V⇩S" and "a ∉ span S" and "dependent (insert a S)"
  shows "dependent S"
    is vector_space.dependent_insertD.

tts_lemma independent_insertI:
  assumes "a ∈ U⇩V⇩S" and "S ⊆ U⇩V⇩S" and "a ∉ span S" and "¬ dependent S"
  shows "¬ dependent (insert a S)"
    is vector_space.independent_insertI.

tts_lemma independent_insert:
  assumes "a ∈ U⇩V⇩S" and "S ⊆ U⇩V⇩S"
  shows "(¬ dependent (insert a S)) = 
    (if a ∈ S then ¬ dependent S else ¬ dependent S ∧ a ∉ span S)"
    is vector_space.independent_insert.

tts_lemma maximal_independent_subset_extend["consumes" - 1, "case_names" "1"]:
  assumes "S ⊆ U⇩V⇩S"
    and "V ⊆ U⇩V⇩S"
    and "S ⊆ V"
    and "¬ dependent S"
    and "⋀B. ⟦B ⊆ U⇩V⇩S; S ⊆ B; B ⊆ V; ¬ dependent B; V ⊆ span B⟧ ⟹ thesis"
  shows thesis
    is vector_space.maximal_independent_subset_extend.

tts_lemma maximal_independent_subset["consumes" - 1, "case_names" "1"]:
  assumes "V ⊆ U⇩V⇩S"
    and "⋀B. ⟦B ⊆ U⇩V⇩S; B ⊆ V; ¬ dependent B; V ⊆ span B⟧ ⟹ thesis"
  shows thesis
    is vector_space.maximal_independent_subset.

tts_lemma in_span_delete:
  assumes "a ∈ U⇩V⇩S"
    and "S ⊆ U⇩V⇩S"
    and "b ∈ U⇩V⇩S"
    and "a ∈ span S"
    and "a ∉ span (S - {b})"
  shows "b ∈ span (insert a (S - {b}))"
    is vector_space.in_span_delete.

tts_lemma span_redundant:
  assumes "x ∈ U⇩V⇩S" and "S ⊆ U⇩V⇩S" and "x ∈ span S"
  shows "span (insert x S) = span S"
    is vector_space.span_redundant.

tts_lemma span_trans:
  assumes "x ∈ U⇩V⇩S"
    and "S ⊆ U⇩V⇩S"
    and "y ∈ U⇩V⇩S"
    and "x ∈ span S"
    and "y ∈ span (insert x S)"
  shows "y ∈ span S"
    is vector_space.span_trans.

tts_lemma span_insert_0:
  assumes "S ⊆ U⇩V⇩S"
  shows "span (insert 0 S) = span S"
    is vector_space.span_insert_0.

tts_lemma span_delete_0:
  assumes "S ⊆ U⇩V⇩S"
  shows "span (S - {0}) = span S"
    is vector_space.span_delete_0.

tts_lemma span_image_scale:
  assumes "S ⊆ U⇩V⇩S" and "finite S" and "⋀x. ⟦x ∈ U⇩V⇩S; x ∈ S⟧ ⟹ c x ≠ 0"
  shows "span ((λx. c x *s x) ` S) = span S"
    is vector_space.span_image_scale.

tts_lemma exchange_lemma:
  assumes "T ⊆ U⇩V⇩S"
    and "S ⊆ U⇩V⇩S"
    and "finite T"
    and "¬dependent S"
    and "S ⊆ span T"
  shows "∃t'∈Pow U⇩V⇩S. 
    card t' = card T ∧ finite t' ∧ S ⊆ t' ∧ t' ⊆ S ∪ T ∧ S ⊆ span t'"
    is vector_space.exchange_lemma.

tts_lemma independent_span_bound:
  assumes "T ⊆ U⇩V⇩S"
    and "S ⊆ U⇩V⇩S"
    and "finite T"
    and "¬ dependent S"
    and "S ⊆ span T"
  shows "finite S ∧ card S ≤ card T"
    is vector_space.independent_span_bound.

tts_lemma independent_explicit_finite_subsets:
  assumes "A ⊆ U⇩V⇩S"
  shows "(¬ dependent A) = 
    (
      ∀x⊆U⇩V⇩S. 
        x ⊆ A ⟶ 
        finite x ⟶ 
        (∀f. (∑v∈x. f v *s v) = 0 ⟶ (∀x∈x. f x = 0))
    )"
    given vector_space.independent_explicit_finite_subsets by auto

tts_lemma independent_if_scalars_zero:
  assumes "A ⊆ U⇩V⇩S"
    and "finite A"
    and "⋀f x. ⟦x ∈ U⇩V⇩S; (∑x∈A. f x *s x) = 0; x ∈ A⟧ ⟹ f x = 0"
  shows "¬ dependent A"
    is vector_space.independent_if_scalars_zero.

tts_lemma subspace_sums:
  assumes "S ⊆ U⇩V⇩S" and "T ⊆ U⇩V⇩S" and "subspace S" and "subspace T"
  shows "subspace {x ∈ U⇩V⇩S. ∃a∈U⇩V⇩S. ∃b∈U⇩V⇩S. x = a + b ∧ a ∈ S ∧ b ∈ T}"
    is vector_space.subspace_sums.

tts_lemma bij_if_span_eq_span_bases:
  assumes "B ⊆ U⇩V⇩S"
    and "C ⊆ U⇩V⇩S"
    and "¬dependent B"
    and "¬dependent C"
    and "span B = span C"
  shows "∃x. bij_betw x B C ∧ (∀a∈U⇩V⇩S. x a ∈ U⇩V⇩S)"
    given vector_space.bij_if_span_eq_span_bases by blast

end

end



subsection‹Transfer: ‹dim››

context vector_space_on
begin

lemma dim_eq_card:
  assumes "B ⊆ U⇩V⇩S"
    and "V ⊆ U⇩V⇩S"
    and BV: "span B = span V" 
    and B: "¬dependent B"
  shows "dim V = card B"
proof-
  define p where "p b ≡ b ⊆ U⇩V⇩S ∧ ¬dependent b ∧ span b = span V" for b
  from assms have "p (SOME B. p B)"
    by (intro someI[of p B], unfold p_def) simp
  then have "∃f. bij_betw f B (SOME B. p B) ∧ (∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S)"
    by (subst (asm) p_def, intro bij_if_span_eq_span_bases) (simp_all add: assms)
  then have "card B = card (SOME B. p B)" by (auto intro: bij_betw_same_card)
  then show ?thesis using assms(1,3,4) unfolding dim_def p_def by auto
qed

lemma dim_transfer[transfer_rule]: 
  includes lifting_syntax                               
  assumes [transfer_domain_rule]: "Domainp A = (λx. x ∈ U⇩V⇩S)"
    and [transfer_rule]: "right_total A" "bi_unique A"
    and [transfer_rule]: "(A ===> A ===> A) plus plus'"
    and [transfer_rule]: "((=) ===> A ===> A) scale scale'"
    and [transfer_rule]: "A 0 zero'"
  shows "(rel_set A ===> (=)) dim (dim.with plus' zero' 0 scale')"
proof(rule rel_funI)
  
  (* preliminaries *)
  have rt_rlA: "right_total (rel_set A)"
    using assms using right_total_rel_set by auto
  have Dom_rsA: "Domainp (rel_set A) x = (x ⊆ U⇩V⇩S)" for x
    by (meson Domainp_set assms(1) in_mono subsetI)

  (* hypothesis and preliminary derived results *)
  fix V V' assume [transfer_rule]: "rel_set A V V'"
  with assms have subset: "V ⊆ U⇩V⇩S" 
    by (metis Domainp.DomainI rel_setD1 subsetI)
  then have "span V ⊆ U⇩V⇩S" by (simp add: span_minimal subspace_UNIV)

  (* convenience definitions *)
  define P' where "P' =
    (
      ∃b. 
        (with 0 zero' plus' scale' : «independent» b) ∧ 
        (with zero' plus' scale' : «span» b) = 
          (with zero' plus' scale' : «span» V')
    )"
  define P where "P = 
    (∃b⊆U⇩V⇩S. ¬ dependent b ∧ span b = span V)"
  have "P = P'" 
    unfolding P_def P'_def by (transfer, unfold tts_implicit) blast
  define f where "f b = (b ⊆ U⇩V⇩S ∧ ¬ dependent b ∧ span b = span V)" for b
  define f' where "f' b = (b ⊆ U⇩V⇩S ∧ f b)" for b
  have "f = f'" unfolding f'_def f_def by simp
  define g where "g b = 
    (
      (with 0 zero' plus' scale' : «independent» b) ∧ 
      (with zero' plus' scale': «span» b) = 
      (with zero' plus' scale' : «span» V')
    )"
    for b
  define g' where "g' b = (b ⊆ UNIV ∧ g b)" for b
  have "g = g'" unfolding g_def g'_def by simp

  (* towards Eps_unique_transfer_lemma *)
  have fg[transfer_rule]: "(rel_set A ===> (=)) f g"
    unfolding ‹g = g'› 
    unfolding f_def g'_def g_def tts_implicit[symmetric]
    apply transfer_prover_start
    apply transfer_step+
    by simp
  have ex_Dom_rsA: "∃x. Domainp (rel_set A) x ∧ f x"
    unfolding Dom_rsA f_def 
    by 
      (
        meson   
          ‹span V ⊆ U⇩V⇩S› 
          maximal_independent_subset 
          span_subspace 
          subspace_span 
          subset
      )
  have card_xy: "⋀x y. ⟦g x; g y⟧ ⟹ card x = card y"
    by (transfer, unfold f_def) (metis dim_eq_card)

  (* main *)
  show "dim V = dim.with plus' zero' 0 scale' V'"
  proof(cases ‹P'›)
    case True
    then have P unfolding ‹P = P'› .
    then have dim: "dim V = card (SOME b. f b)"
      unfolding dim_def P_def f_def by simp
    from True have dw: "dim.with plus' zero' 0 scale' V' = card (SOME b. g b)"
      unfolding dim.with_def P'_def g_def by simp
    from Eps_unique_transfer_lemma[
        OF rt_rlA fg card_transfer[OF ‹bi_unique A›] ex_Dom_rsA card_xy, 
        simplified,
        unfolded Dom_rsA,
        folded f'_def ‹f = f'›
        ]
    show "dim V = dim.with plus' zero' 0 scale' V'" 
      unfolding dim dw by simp
  next
    case False
    then have "¬P" unfolding ‹P = P'› .
    then have dim: "dim V = 0" unfolding dim_def P_def by auto 
    moreover from False have dw: "dim.with plus' zero'  0 scale' V' = 0"
      unfolding dim.with_def P'_def g_def by auto
    ultimately show ?thesis by simp
  qed

qed

end



subsection‹Relativization: part II›

context vector_space_on
begin

tts_context
  tts: (?'b to ‹U⇩V⇩S::'b set›)
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and 
      (
        ‹?scale::?'a::field ⇒?'b::ab_group_add⇒?'b::ab_group_add› to 
        ‹(*s)::'a⇒'b⇒'b›
      )
    and (‹0::?'b::ab_group_add› to ‹0::'b›)
  rewriting ctr_simps
  substituting ab_group_add_ow_axioms 
    and vector_space_ow_axioms
    and implicit⇩M.module_ow_axioms
  eliminating ‹?a ∈ ?A› and ‹?B ⊆ ?C› through auto
  applying 
    [
      OF 
        implicit⇩M.carrier_ne 
        implicit⇩V⇩S.minus_closed' 
        implicit⇩V⇩S.uminus_closed', 
      unfolded tts_implicit
     ]
begin

tts_lemma dim_unique:
  assumes "V ⊆ U⇩V⇩S"
    and "B ⊆ V"
    and "V ⊆ span B"
    and "¬ dependent B"
    and "card B = n"
  shows "dim V = n"
    is vector_space.dim_unique.
    
tts_lemma basis_card_eq_dim:
  assumes "V ⊆ U⇩V⇩S" and "B ⊆ V" and "V ⊆ span B" and "¬ dependent B"
  shows "card B = dim V"
    is vector_space.basis_card_eq_dim.
    
tts_lemma dim_eq_card_independent:
  assumes "B ⊆ U⇩V⇩S" and "¬ dependent B"
  shows "dim B = card B"
    is vector_space.dim_eq_card_independent.

tts_lemma dim_span:
  assumes "S ⊆ U⇩V⇩S"
  shows "dim (span S) = dim S"
    is vector_space.dim_span.

tts_lemma dim_span_eq_card_independent:
  assumes "B ⊆ U⇩V⇩S" and "¬ dependent B"
  shows "dim (span B) = card B"
    is vector_space.dim_span_eq_card_independent.

tts_lemma dim_le_card:
  assumes "V ⊆ U⇩V⇩S" and "W ⊆ U⇩V⇩S" and "V ⊆ span W" and "finite W"
  shows "dim V ≤ card W"
    is vector_space.dim_le_card.

tts_lemma span_eq_dim:
  assumes "S ⊆ U⇩V⇩S" and "T ⊆ U⇩V⇩S" and "span S = span T"
  shows "dim S = dim T"
    is vector_space.span_eq_dim.

tts_lemma dim_le_card':
  assumes "s ⊆ U⇩V⇩S" and "finite s"
  shows "dim s ≤ card s"
    is vector_space.dim_le_card'.

tts_lemma span_card_ge_dim:
  assumes "V ⊆ U⇩V⇩S" and "B ⊆ V" and "V ⊆ span B" and "finite B"
  shows "dim V ≤ card B"
    is vector_space.span_card_ge_dim.

end

tts_context
  tts: (?'b to ‹U⇩V⇩S::'b set›) 
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and (‹?scale::?'a::field ⇒?'b::ab_group_add⇒?'b› to ‹(*s)::'a⇒'b⇒'b›)
    and (‹0::?'b::ab_group_add› to ‹0::'b›)
  rewriting ctr_simps
  substituting ab_group_add_ow_axioms 
    and vector_space_ow_axioms
    and implicit⇩M.module_ow_axioms
  applying 
    [
      OF 
        implicit⇩M.carrier_ne 
        implicit⇩V⇩S.minus_closed' 
        implicit⇩V⇩S.uminus_closed', 
        unfolded tts_implicit
     ]
begin
  
tts_lemma basis_exists:
  assumes "V ⊆ U⇩V⇩S"
    and "⋀B. 
      ⟦
        B ⊆ U⇩V⇩S; 
        B ⊆ V; 
        ¬ dependent B; 
        V ⊆ span B; 
        card B = dim V
      ⟧ ⟹ thesis"
  shows thesis
    is vector_space.basis_exists.

end

end

context finite_dimensional_vector_space_on 
begin

tts_context
  tts: (?'b to ‹U⇩V⇩S::'b set›)
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and (‹?scale::?'a::field ⇒?'b::ab_group_add⇒?'b› to ‹(*s)::'a⇒'b⇒'b›)
    and (‹0::?'b::ab_group_add› to ‹0::'b›)
  rewriting ctr_simps
  substituting ab_group_add_ow_axioms
    and vector_space_ow_axioms
    and implicit⇩V⇩S.finite_dimensional_vector_space_ow_axioms
    and implicit⇩M.module_ow_axioms
  eliminating ‹?a ∈ ?A› and ‹?B ⊆ ?C› through auto
  applying 
    [
      OF 
        implicit⇩M.carrier_ne 
        implicit⇩V⇩S.minus_closed' 
        implicit⇩V⇩S.uminus_closed' 
        basis_subset, 
      unfolded tts_implicit
    ]
begin

tts_lemma finiteI_independent:
  assumes "B ⊆ U⇩V⇩S" and "¬ dependent B"
  shows "finite B"
  is finite_dimensional_vector_space.finiteI_independent.

tts_lemma dim_empty: "dim {} = 0"
  is finite_dimensional_vector_space.dim_empty.
    
tts_lemma dim_insert:
  assumes "x ∈ U⇩V⇩S" and "S ⊆ U⇩V⇩S"
  shows "dim (insert x S) = (if x ∈ span S then dim S else dim S + 1)"
    is finite_dimensional_vector_space.dim_insert.
    
tts_lemma dim_singleton:
  assumes "x ∈ U⇩V⇩S"
  shows "dim {x} = (if x = 0 then 0 else 1)"
    is finite_dimensional_vector_space.dim_singleton.

tts_lemma choose_subspace_of_subspace["consumes" - 1, "case_names" "1"]:
  assumes "S ⊆ U⇩V⇩S"
    and "n ≤ dim S"
    and "⋀T. ⟦T ⊆ U⇩V⇩S; subspace T; T ⊆ span S; dim T = n⟧ ⟹ thesis"
  shows thesis
    is finite_dimensional_vector_space.choose_subspace_of_subspace.

tts_lemma basis_subspace_exists["consumes" - 1, "case_names" "1"]:
  assumes "S ⊆ U⇩V⇩S"
    and "subspace S"
    and "⋀B. 
      ⟦
        B ⊆ U⇩V⇩S; 
        finite B; 
        B ⊆ S; 
        ¬ dependent B; 
        span B = S; 
        card B = dim S
      ⟧ ⟹ thesis"
  shows thesis
    is finite_dimensional_vector_space.basis_subspace_exists.

tts_lemma dim_mono:
  assumes "V ⊆ U⇩V⇩S" and "W ⊆ U⇩V⇩S" and "V ⊆ span W"
  shows "dim V ≤ dim W"
    is finite_dimensional_vector_space.dim_mono.

tts_lemma dim_subset:
  assumes "T ⊆ U⇩V⇩S" and "S ⊆ T"
  shows "dim S ≤ dim T"
    is finite_dimensional_vector_space.dim_subset.

tts_lemma dim_eq_0:
  assumes "S ⊆ U⇩V⇩S"
  shows "(dim S = 0) = (S ⊆ {0})"
    is finite_dimensional_vector_space.dim_eq_0.

tts_lemma dim_UNIV: "dim U⇩V⇩S = card basis"
    is finite_dimensional_vector_space.dim_UNIV.

tts_lemma independent_card_le_dim:
  assumes "V ⊆ U⇩V⇩S" and "B ⊆ V" and "¬ dependent B"
  shows "card B ≤ dim V"
    is finite_dimensional_vector_space.independent_card_le_dim.

tts_lemma card_ge_dim_independent:
  assumes "V ⊆ U⇩V⇩S" and "B ⊆ V" and "¬ dependent B" and "dim V ≤ card B"
  shows "V ⊆ span B"
    is finite_dimensional_vector_space.card_ge_dim_independent.

tts_lemma card_le_dim_spanning:
  assumes "V ⊆ U⇩V⇩S"
    and "B ⊆ V"
    and "V ⊆ span B"
    and "finite B"
    and "card B ≤ dim V"
  shows "¬ dependent B"
    is finite_dimensional_vector_space.card_le_dim_spanning.

tts_lemma card_eq_dim:
  assumes "V ⊆ U⇩V⇩S" and "B ⊆ V" and "card B = dim V" and "finite B"
  shows "(¬ dependent B) = (V ⊆ span B)"
    is finite_dimensional_vector_space.card_eq_dim.

tts_lemma subspace_dim_equal:
  assumes "T ⊆ U⇩V⇩S"
    and "subspace S"
    and "subspace T"
    and "S ⊆ T"
    and "dim T ≤ dim S"
  shows "S = T"
    is finite_dimensional_vector_space.subspace_dim_equal.

tts_lemma dim_eq_span:
  assumes "T ⊆ U⇩V⇩S" and "S ⊆ T" and "dim T ≤ dim S"
  shows "span S = span T"
    is finite_dimensional_vector_space.dim_eq_span.

tts_lemma dim_psubset:
  assumes "S ⊆ U⇩V⇩S" and "T ⊆ U⇩V⇩S" and "span S ⊂ span T"
  shows "dim S < dim T"
    is finite_dimensional_vector_space.dim_psubset.

tts_lemma indep_card_eq_dim_span:
  assumes "B ⊆ U⇩V⇩S" and "¬ dependent B"
  shows "finite B ∧ card B = dim (span B)"
    is finite_dimensional_vector_space.indep_card_eq_dim_span.

tts_lemma independent_bound_general:
  assumes "S ⊆ U⇩V⇩S" and "¬ dependent S"
  shows "finite S ∧ card S ≤ dim S"
    is finite_dimensional_vector_space.independent_bound_general.

tts_lemma independent_explicit:
  assumes "B ⊆ U⇩V⇩S"
  shows "(¬ dependent B) = 
    (finite B ∧ (∀x. (∑v∈B. x v *s v) = 0 ⟶ (∀a∈B. x a = 0)))"
    is finite_dimensional_vector_space.independent_explicit.

tts_lemma dim_sums_Int:
  assumes "S ⊆ U⇩V⇩S" and "T ⊆ U⇩V⇩S" and "subspace S" and "subspace T"
  shows 
    "dim {x ∈ U⇩V⇩S. ∃y∈U⇩V⇩S. ∃z∈U⇩V⇩S. x = y + z ∧ y ∈ S ∧ z ∈ T} + dim (S ∩ T) = 
      dim S + dim T"
    is finite_dimensional_vector_space.dim_sums_Int.

tts_lemma dependent_biggerset_general:
  assumes "S ⊆ U⇩V⇩S" and "finite S ⟹ dim S < card S"
  shows "dependent S"
    is finite_dimensional_vector_space.dependent_biggerset_general.

tts_lemma subset_le_dim:
  assumes "S ⊆ U⇩V⇩S" and "T ⊆ U⇩V⇩S" and "S ⊆ span T"
  shows "dim S ≤ dim T"
    is finite_dimensional_vector_space.subset_le_dim.

tts_lemma linear_inj_imp_surj:
  assumes "∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f"
    and "inj_on f U⇩V⇩S"
  shows "f ` U⇩V⇩S = U⇩V⇩S"
    is finite_dimensional_vector_space.linear_inj_imp_surj.

tts_lemma linear_surj_imp_inj:
  assumes "∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f"
    and "f ` U⇩V⇩S = U⇩V⇩S"
  shows "inj_on f U⇩V⇩S"
    is finite_dimensional_vector_space.linear_surj_imp_inj.

tts_lemma linear_inverse_left:
  assumes "∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S"
    and "∀x∈U⇩V⇩S. f' x ∈ U⇩V⇩S"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f'"
  shows "(∀x∈U⇩V⇩S. (f ∘ f') x = id x) = (∀x∈U⇩V⇩S. (f' ∘ f) x = id x)"
    is finite_dimensional_vector_space.linear_inverse_left[unfolded fun_eq_iff].

tts_lemma left_inverse_linear:
  assumes "∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S"
    and "∀x∈U⇩V⇩S. g x ∈ U⇩V⇩S"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f"
    and "∀x∈U⇩V⇩S. (g ∘ f) x = id x"
  shows "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) g"
    is finite_dimensional_vector_space.left_inverse_linear[unfolded fun_eq_iff].

tts_lemma right_inverse_linear:
  assumes "∀x∈U⇩V⇩S. f x ∈ U⇩V⇩S"
    and "∀x∈U⇩V⇩S. g x ∈ U⇩V⇩S"
    and "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) f"
    and "∀x∈U⇩V⇩S. (f ∘ g) x = id x"
  shows "linear_on U⇩V⇩S U⇩V⇩S (*s) (*s) g"
    is finite_dimensional_vector_space.right_inverse_linear[unfolded fun_eq_iff].

end

end

context vector_space_pair_on 
begin

tts_context
  tts: (?'b to ‹U⇩M⇩_⇩1::'b set›) and (?'c to ‹U⇩M⇩_⇩2::'c set›) 
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and (‹?s1.0::?'a::field ⇒?'b::ab_group_add⇒?'b› to ‹(*s⇩1)::'a⇒'b⇒'b›)
    and (‹0::?'b::ab_group_add› to ‹0::'b›) 
    and (‹(+)::?'c::ab_group_add⇒?'c⇒?'c› to ‹(+)::'c⇒'c⇒'c›)
    and (‹?s2.0::?'a::field ⇒?'c::ab_group_add⇒?'c› to ‹(*s⇩2)::'a⇒'c⇒'c›)
    and (‹0::?'c::ab_group_add› to ‹0::'c›)
  rewriting ctr_simps
  substituting VS⇩1.ab_group_add_ow_axioms
    and VS⇩1.vector_space_ow_axioms
    and VS⇩2.ab_group_add_ow_axioms
    and VS⇩2.vector_space_ow_axioms
    and implicit⇩V⇩S.vector_space_pair_ow_axioms
    and VS⇩1.implicit⇩M.module_ow_axioms
    and VS⇩2.implicit⇩M.module_ow_axioms
  eliminating ‹?a ∈ U⇩M⇩_⇩1› and ‹?B ⊆ U⇩M⇩_⇩1› and ‹?a ∈ U⇩M⇩_⇩2› and ‹?B ⊆ U⇩M⇩_⇩2› 
    through auto
  applying  
    [
      OF 
        VS⇩1.implicit⇩M.carrier_ne VS⇩2.implicit⇩M.carrier_ne 
        VS⇩1.implicit⇩M.minus_closed' VS⇩1.implicit⇩M.uminus_closed' 
        VS⇩2.implicit⇩V⇩S.minus_closed' VS⇩2.implicit⇩V⇩S.uminus_closed',
      unfolded tts_implicit
    ]
begin

tts_lemma linear_add:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "b1 ∈ U⇩M⇩_⇩1"
    and "b2 ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "f (b1 + b2) = f b1 + f b2"
    is vector_space_pair.linear_add.

tts_lemma linear_scale:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "b ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "f (r *s⇩1 b) = r *s⇩2 f b"
    is vector_space_pair.linear_scale.
    
tts_lemma linear_neg:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "x ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "f (- x) = - f x"
    is vector_space_pair.linear_neg.
    
tts_lemma linear_diff:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "x ∈ U⇩M⇩_⇩1"
    and "y ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "f (x - y) = f x - f y"
    is vector_space_pair.linear_diff.
    
tts_lemma linear_sum:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "range g ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "f (sum g S) = (∑a∈S. f (g a))"
is vector_space_pair.linear_sum.

tts_lemma linear_inj_on_iff_eq_0:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "s ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩1.subspace s"
  shows "inj_on f s = (∀x∈s. f x = 0 ⟶ x = 0)"
    is vector_space_pair.linear_inj_on_iff_eq_0.

tts_lemma linear_inj_iff_eq_0:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "inj_on f U⇩M⇩_⇩1 = (∀x∈U⇩M⇩_⇩1. f x = 0 ⟶ x = 0)"
    is vector_space_pair.linear_inj_iff_eq_0.

tts_lemma linear_subspace_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩1.subspace S"
  shows "VS⇩2.subspace (f ` S)"
    is vector_space_pair.linear_subspace_image.

tts_lemma linear_subspace_kernel:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "VS⇩1.subspace {x ∈ U⇩M⇩_⇩1. f x = 0}"
    is vector_space_pair.linear_subspace_kernel.

tts_lemma linear_span_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "VS⇩2.span (f ` S) = f ` VS⇩1.span S"
    is vector_space_pair.linear_span_image.

tts_lemma linear_dependent_inj_imageD:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "s ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩2.dependent (f ` s)"
    and "inj_on f (VS⇩1.span s)"
  shows "VS⇩1.dependent s"
    is vector_space_pair.linear_dependent_inj_imageD.

tts_lemma linear_eq_0_on_span:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "b ⊆ U⇩M⇩_⇩1"
    and "x ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "⋀x. ⟦x ∈ U⇩M⇩_⇩1; x ∈ b⟧ ⟹ f x = 0"
    and "x ∈ VS⇩1.span b"
  shows "f x = 0"
    is vector_space_pair.linear_eq_0_on_span.

tts_lemma linear_independent_injective_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "s ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "¬ VS⇩1.dependent s"
    and "inj_on f (VS⇩1.span s)"
  shows "¬ VS⇩2.dependent (f ` s)"
    is vector_space_pair.linear_independent_injective_image.

tts_lemma linear_inj_on_span_independent_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "B ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "¬ VS⇩2.dependent (f ` B)"
    and "inj_on f B"
  shows "inj_on f (VS⇩1.span B)"
    is vector_space_pair.linear_inj_on_span_independent_image.

tts_lemma linear_inj_on_span_iff_independent_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "B ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "¬ VS⇩2.dependent (f ` B)"
  shows "inj_on f (VS⇩1.span B) = inj_on f B"
    is vector_space_pair.linear_inj_on_span_iff_independent_image.

tts_lemma linear_subspace_linear_preimage:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩2.subspace S"
  shows "VS⇩1.subspace {x ∈ U⇩M⇩_⇩1. f x ∈ S}"
    is vector_space_pair.linear_subspace_linear_preimage.

tts_lemma linear_spans_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "V ⊆ U⇩M⇩_⇩1"
    and "B ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "V ⊆ VS⇩1.span B"
  shows "f ` V ⊆ VS⇩2.span (f ` B)"
    is vector_space_pair.linear_spans_image.

tts_lemma linear_spanning_surjective_image:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "U⇩M⇩_⇩1 ⊆ VS⇩1.span S"
    and "f ` U⇩M⇩_⇩1 = U⇩M⇩_⇩2"
  shows "U⇩M⇩_⇩2 ⊆ VS⇩2.span (f ` S)"
    is vector_space_pair.linear_spanning_surjective_image.

tts_lemma linear_eq_on_span:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
    and "B ⊆ U⇩M⇩_⇩1"
    and "x ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
    and "⋀x. ⟦x ∈ U⇩M⇩_⇩1; x ∈ B⟧ ⟹ f x = g x"
    and "x ∈ VS⇩1.span B"
  shows "f x = g x"
    is vector_space_pair.linear_eq_on_span.

tts_lemma linear_compose_scale_right:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. c *s⇩2 f x)"
    is vector_space_pair.linear_compose_scale_right.

tts_lemma linear_compose_add:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x + g x)"
    is vector_space_pair.linear_compose_add.

tts_lemma linear_zero:
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. 0)"
    is vector_space_pair.linear_zero.

tts_lemma linear_compose_sub:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x - g x)"
    is vector_space_pair.linear_compose_sub.

tts_lemma linear_compose_neg:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. - f x)"
    is vector_space_pair.linear_compose_neg.

tts_lemma linear_compose_scale:
  assumes "c ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 UNIV (*s⇩1) (*) f"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x *s⇩2 c)"
    is vector_space_pair.linear_compose_scale.

tts_lemma linear_indep_image_lemma:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "B ⊆ U⇩M⇩_⇩1"
    and "x ∈ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "finite B"
    and "¬ VS⇩2.dependent (f ` B)"
    and "inj_on f B"
    and "x ∈ VS⇩1.span B"
    and "f x = 0"
  shows "x = 0"
    is vector_space_pair.linear_indep_image_lemma.

tts_lemma linear_eq_on:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
    and "x ∈ U⇩M⇩_⇩1"
    and "B ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
    and "x ∈ VS⇩1.span B"
    and "⋀b. ⟦b ∈ U⇩M⇩_⇩1; b ∈ B⟧ ⟹ f b = g b"
  shows "f x = g x"
    is vector_space_pair.linear_eq_on.

tts_lemma linear_compose_sum:
  assumes "∀x. ∀y∈U⇩M⇩_⇩1. f x y ∈ U⇩M⇩_⇩2"
    and "∀x∈S. linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (f x)"
  shows "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. ∑a∈S. f a x)"
    is vector_space_pair.linear_compose_sum.

tts_lemma linear_independent_extend_subspace:
  assumes "B ⊆ U⇩M⇩_⇩1"
    and "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "¬ VS⇩1.dependent B"
  shows 
    "∃x.
      (∀a∈U⇩M⇩_⇩1. x a ∈ U⇩M⇩_⇩2) ∧ 
      linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) x ∧ 
      (∀a∈B. x a = f a) ∧ 
      x ` U⇩M⇩_⇩1 = VS⇩2.span (f ` B)"
    given vector_space_pair.linear_independent_extend_subspace by auto

tts_lemma linear_independent_extend:
  assumes "B ⊆ U⇩M⇩_⇩1"
    and "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "¬ VS⇩1.dependent B"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩1. x a ∈ U⇩M⇩_⇩2) ∧ 
      (∀a∈B. x a = f a) ∧ 
      linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) x"
    given vector_space_pair.linear_independent_extend by auto

tts_lemma linear_exists_left_inverse_on:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "V ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩1.subspace V"
    and "inj_on f V"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      x ` U⇩M⇩_⇩2 ⊆ V ∧ 
      (∀a∈V. x (f a) = a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_exists_left_inverse_on by auto

tts_lemma linear_exists_right_inverse_on:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "V ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩1.subspace V"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      x ` U⇩M⇩_⇩2 ⊆ V ∧ 
      (∀a∈f ` V. f (x a) = a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_exists_right_inverse_on by auto

tts_lemma linear_inj_on_left_inverse:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "inj_on f (VS⇩1.span S)"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      x ` U⇩M⇩_⇩2 ⊆ VS⇩1.span S ∧ 
      (∀a∈VS⇩1.span S. x (f a) = a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_inj_on_left_inverse by auto

tts_lemma linear_surj_right_inverse:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "T ⊆ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩2.span T ⊆ f ` VS⇩1.span S"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      x ` U⇩M⇩_⇩2 ⊆ VS⇩1.span S ∧ 
      (∀a∈VS⇩2.span T. f (x a) = a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_surj_right_inverse by auto

tts_lemma finite_basis_to_basis_subspace_isomorphism:
  assumes "S ⊆ U⇩M⇩_⇩1"
    and "T ⊆ U⇩M⇩_⇩2"
    and "VS⇩1.subspace S"
    and "VS⇩2.subspace T"
    and "VS⇩1.dim S = VS⇩2.dim T"
    and "finite B"
    and "B ⊆ S"
    and "¬ VS⇩1.dependent B"
    and "S ⊆ VS⇩1.span B"
    and "card B = VS⇩1.dim S"
    and "finite C"
    and "C ⊆ T"
    and "¬ VS⇩2.dependent C"
    and "T ⊆ VS⇩2.span C"
    and "card C = VS⇩2.dim T"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩1. x a ∈ U⇩M⇩_⇩2) ∧ 
      linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) x ∧ 
      x ` B = C ∧ 
      inj_on x S ∧ x ` S = T"
    given vector_space_pair.finite_basis_to_basis_subspace_isomorphism by auto

tts_lemma linear_subspace_vimage:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "VS⇩2.subspace S"
  shows "VS⇩1.subspace (f -` S ∩ U⇩M⇩_⇩1)"
    is vector_space_pair.linear_subspace_vimage.

tts_lemma linear_injective_left_inverse:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "inj_on f U⇩M⇩_⇩1"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      (∀a∈U⇩M⇩_⇩1. (x ∘ f) a = id a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_injective_left_inverse[unfolded fun_eq_iff]
  by auto

tts_lemma linear_surjective_right_inverse:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "f ` U⇩M⇩_⇩1 = U⇩M⇩_⇩2"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      (∀a∈U⇩M⇩_⇩2. (f ∘ x) a = id a) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x"
    given vector_space_pair.linear_surjective_right_inverse[unfolded fun_eq_iff]
  by auto

end

end

context finite_dimensional_vector_space_pair_1_on 
begin

tts_context
  tts: (?'b to ‹U⇩M⇩_⇩1::'b set›) and (?'c to ‹U⇩M⇩_⇩2::'c set›) 
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and (‹?s1.0::?'a::field ⇒?'b::ab_group_add⇒?'b› to ‹(*s⇩1)::'a⇒'b⇒'b›)
    and (‹0::?'b::ab_group_add› to ‹0::'b›) 
    and (‹(+)::?'c::ab_group_add⇒?'c⇒?'c› to ‹(+)::'c⇒'c⇒'c›)
    and (‹?s2.0::?'a::field ⇒?'c::ab_group_add⇒?'c› to ‹(*s⇩2)::'a⇒'c⇒'c›)
    and (‹0::?'c::ab_group_add› to ‹0::'c›)
  rewriting ctr_simps
  substituting VS⇩1.ab_group_add_ow_axioms
    and VS⇩1.vector_space_ow_axioms
    and VS⇩2.ab_group_add_ow_axioms
    and VS⇩2.vector_space_ow_axioms
    and implicit⇩V⇩S.vector_space_pair_ow_axioms
    and VS⇩1.implicit⇩M.module_ow_axioms
    and VS⇩2.implicit⇩M.module_ow_axioms 
    and implicit⇩V⇩S.finite_dimensional_vector_space_pair_1_ow_axioms
  applying  
    [
      OF 
        VS⇩1.implicit⇩M.carrier_ne VS⇩2.implicit⇩M.carrier_ne 
        VS⇩1.implicit⇩V⇩S.minus_closed' VS⇩1.implicit⇩V⇩S.uminus_closed' 
        VS⇩2.implicit⇩V⇩S.minus_closed' VS⇩2.implicit⇩V⇩S.uminus_closed'
        VS⇩1.basis_subset,
      unfolded tts_implicit
    ]
begin

tts_lemma lt_dim_image_eq:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "inj_on f (VS⇩1.span S)"
  shows "VS⇩2.dim (f ` S) = VS⇩1.dim S"
    is finite_dimensional_vector_space_pair_1.dim_image_eq.

tts_lemma lt_dim_image_le:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "S ⊆ U⇩M⇩_⇩1"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
  shows "VS⇩2.dim (f ` S) ≤ VS⇩1.dim S"
    is finite_dimensional_vector_space_pair_1.dim_image_le.

end

end

context finite_dimensional_vector_space_pair_on 
begin

tts_context
  tts: (?'b to ‹U⇩M⇩_⇩1::'b set›) and (?'c to ‹U⇩M⇩_⇩2::'c set›) 
  sbterms: (‹(+)::?'b::ab_group_add⇒?'b⇒?'b› to ‹(+)::'b⇒'b⇒'b›)
    and (‹?s1.0::?'a::field ⇒?'b::ab_group_add⇒?'b› to ‹(*s⇩1)::'a⇒'b⇒'b›)
    and (‹0::?'b::ab_group_add› to ‹0::'b›) 
    and (‹(+)::?'c::ab_group_add⇒?'c⇒?'c› to ‹(+)::'c⇒'c⇒'c›)
    and (‹?s2.0::?'a::field ⇒?'c::ab_group_add⇒?'c› to ‹(*s⇩2)::'a⇒'c⇒'c›)
    and (‹0::?'c::ab_group_add› to ‹0::'c›)
  rewriting ctr_simps
  substituting VS⇩1.ab_group_add_ow_axioms
    and VS⇩1.vector_space_ow_axioms
    and VS⇩2.ab_group_add_ow_axioms
    and VS⇩2.vector_space_ow_axioms
    and implicit⇩V⇩S.vector_space_pair_ow_axioms
    and VS⇩1.implicit⇩M.module_ow_axioms
    and VS⇩2.implicit⇩M.module_ow_axioms 
    and implicit⇩V⇩S.finite_dimensional_vector_space_pair_ow_axioms
  applying  
    [
      OF 
        VS⇩1.implicit⇩M.carrier_ne VS⇩2.implicit⇩M.carrier_ne 
        VS⇩1.implicit⇩V⇩S.minus_closed' VS⇩1.implicit⇩V⇩S.uminus_closed' 
        VS⇩2.implicit⇩V⇩S.minus_closed' VS⇩2.implicit⇩V⇩S.uminus_closed'
        VS⇩1.basis_subset VS⇩2.basis_subset,
      unfolded tts_implicit
    ]
begin

tts_lemma linear_surjective_imp_injective:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "f ` U⇩M⇩_⇩1 = U⇩M⇩_⇩2"
    and "VS⇩2.dim U⇩M⇩_⇩2 = VS⇩1.dim U⇩M⇩_⇩1"
  shows "inj_on f U⇩M⇩_⇩1"
    is finite_dimensional_vector_space_pair.linear_surjective_imp_injective.

tts_lemma linear_injective_imp_surjective:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "inj_on f U⇩M⇩_⇩1"
    and "VS⇩2.dim U⇩M⇩_⇩2 = VS⇩1.dim U⇩M⇩_⇩1"
  shows "f ` U⇩M⇩_⇩1 = U⇩M⇩_⇩2"
    is finite_dimensional_vector_space_pair.linear_injective_imp_surjective.

tts_lemma linear_injective_isomorphism:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "inj_on f U⇩M⇩_⇩1"
    and "VS⇩2.dim U⇩M⇩_⇩2 = VS⇩1.dim U⇩M⇩_⇩1"
  shows 
    "∃x. 
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x ∧ 
      (∀a∈U⇩M⇩_⇩1. x (f a) = a) ∧ 
      (∀a∈U⇩M⇩_⇩2. f (x a) = a)"
    given finite_dimensional_vector_space_pair.linear_injective_isomorphism
  by auto

tts_lemma linear_surjective_isomorphism:
  assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
    and "linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
    and "f ` U⇩M⇩_⇩1 = U⇩M⇩_⇩2"
    and "VS⇩2.dim U⇩M⇩_⇩2 = VS⇩1.dim U⇩M⇩_⇩1"
  shows 
    "∃x.
      (∀a∈U⇩M⇩_⇩2. x a ∈ U⇩M⇩_⇩1) ∧ 
      linear_on U⇩M⇩_⇩2 U⇩M⇩_⇩1 (*s⇩2) (*s⇩1) x ∧ 
      (∀a∈U⇩M⇩_⇩1. x (f a) = a) ∧ 
      (∀a∈U⇩M⇩_⇩2. f (x a) = a)"
    given finite_dimensional_vector_space_pair.linear_surjective_isomorphism
  by auto

tts_lemma basis_to_basis_subspace_isomorphism:
  assumes "S ⊆ U⇩M⇩_⇩1"
    and "T ⊆ U⇩M⇩_⇩2"
    and "B ⊆ U⇩M⇩_⇩1"
    and "C ⊆ U⇩M⇩_⇩2"
    and "VS⇩1.subspace S"
    and "VS⇩2.subspace T"
    and "VS⇩1.dim S = VS⇩2.dim T"
    and "B ⊆ S"
    and "¬ VS⇩1.dependent B"
    and "S ⊆ VS⇩1.span B"
    and "card B = VS⇩1.dim S"
    and "C ⊆ T"
    and "¬ VS⇩2.dependent C"
    and "T ⊆ VS⇩2.span C"
    and "card C = VS⇩2.dim T"
  shows
    "∃x.
      (∀a∈U⇩M⇩_⇩1. x a ∈ U⇩M⇩_⇩2) ∧
      linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) x ∧
      x ` B = C ∧
      inj_on x S ∧
      x ` S = T"
  given finite_dimensional_vector_space_pair.basis_to_basis_subspace_isomorphism
  by auto

tts_lemma subspace_isomorphism:
  assumes "S ⊆ U⇩M⇩_⇩1"
    and "T ⊆ U⇩M⇩_⇩2"
    and "VS⇩1.subspace S"
    and "VS⇩2.subspace T"
    and "VS⇩1.dim S = VS⇩2.dim T"
  shows "∃x.
    (∀a∈U⇩M⇩_⇩1. x a ∈ U⇩M⇩_⇩2) ∧
    (inj_on x S ∧ x ` S = T) ∧
    linear_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) x"
    given finite_dimensional_vector_space_pair.subspace_isomorphism by auto

end

end

text‹\newpage›

end