# Theory VS_Vector_Spaces

```(* Title: Examples/Vector_Spaces/VS_Vector_Spaces.thy
Author: 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

"vector_space = vector_space_with (+) 0 (-) uminus"
unfolding vector_space_def vector_space_with_def vector_space_with_axioms_def

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)

"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
..

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"

"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
..

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"

"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:
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)

"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

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

"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
..

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"

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

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
(
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
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
(
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
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
and vector_space_ow_axioms
and implicit⇩M.module_ow_axioms
applying
[
OF
implicit⇩M.carrier_ne
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›)
and
(
‹(*s)::'a⇒'b⇒'b›
)
rewriting ctr_simps
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›)
rewriting ctr_simps
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›)
rewriting ctr_simps
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›)
rewriting ctr_simps
and VS⇩1.vector_space_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

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"

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.

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

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 ⊆```