:: VECTSP_5 semantic presentation

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃, c₄ be Subspace of c₂;
func c₃ + c₄ -> strict Subspace of a₂ means :Def1: :: VECTSP_5:def 1
the carrier of a₅ = { (b₁ + b₂) where B is Element of a₂, B is Element of a₂ : ( b₁ in a₃ & b₂ in a₄ ) } ;
existence

proof end;

uniqueness by VECTSP_4:37;

end;

:: deftheorem Def1 defines + VECTSP_5:def 1 :

Lemma2: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds b₃ + b₄ = b₄ + b₃

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃, c₄ be Subspace of c₂;
func c₃ /\ c₄ -> strict Subspace of a₂ means :Def2: :: VECTSP_5:def 2
the carrier of a₅ = the carrier of a₃ /\ the carrier of a₄;
existence

proof end;

uniqueness by VECTSP_4:37;
commutativity ;

end;

:: deftheorem Def2 defines /\ VECTSP_5:def 2 :

theorem Th1: :: VECTSP_5:1

canceled;

theorem Th2: :: VECTSP_5:2

canceled;

theorem Th3: :: VECTSP_5:3

canceled;

theorem Th4: :: VECTSP_5:4

canceled;

theorem Th5: :: VECTSP_5:5

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being set holds
( b₅ in b₃ + b₄ iff ex b₆, b₇ being Element of b₂ st
( b₆ in b₃ & b₇ in b₄ & b₅ = b₆ + b₇ ) )

proof end;

theorem Th6: :: VECTSP_5:6

proof end;

theorem Th7: :: VECTSP_5:7

proof end;

Lemma7: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds the carrier of b₃ c= the carrier of (b₃ + b₄)

proof end;

Lemma8: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subspace of b₂
for b₄ being strict Subspace of b₂ st the carrier of b₃ c= the carrier of b₄ holds
b₃ + b₄ = b₄

proof end;

theorem Th8: :: VECTSP_5:8

theorem Th9: :: VECTSP_5:9

theorem Th10: :: VECTSP_5:10

proof end;

theorem Th11: :: VECTSP_5:11

proof end;

theorem Th12: :: VECTSP_5:12

proof end;

theorem Th13: :: VECTSP_5:13

proof end;

Lemma13: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subspace of b₂ ex b₄ being strict Subspace of b₂ st the carrier of b₃ = the carrier of b₄

proof end;

Lemma14: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ st the carrier of b₃ = the carrier of b₄ holds
( b₅ + b₃ = b₅ + b₄ & b₃ + b₅ = b₄ + b₅ )

proof end;

Lemma15: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subspace of b₂ holds b₃ is Subspace of (Omega). b₂

proof end;

theorem Th14: :: VECTSP_5:14

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁ holds
( ((0). b₂) + ((Omega). b₂) = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) & ((Omega). b₂) + ((0). b₂) = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) ) by Th13;

theorem Th15: :: VECTSP_5:15

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subspace of b₂ holds
( ((Omega). b₂) + b₃ = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) & b₃ + ((Omega). b₂) = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) )

proof end;

theorem Th16: :: VECTSP_5:16

theorem Th17: :: VECTSP_5:17

proof end;

theorem Th18: :: VECTSP_5:18

canceled;

theorem Th19: :: VECTSP_5:19

proof end;

Lemma19: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds the carrier of (b₃ /\ b₄) c= the carrier of b₃

proof end;

theorem Th20: :: VECTSP_5:20

proof end;

Lemma21: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ st the carrier of b₃ = the carrier of b₄ holds
( b₅ /\ b₃ = b₅ /\ b₄ & b₃ /\ b₅ = b₄ /\ b₅ )

proof end;

theorem Th21: :: VECTSP_5:21

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃ being Subspace of b₂ holds
( ( for b₄ being strict Subspace of b₂ st b₄ is Subspace of b₃ holds
b₄ /\ b₃ = b₄ ) & ( for b₄ being Subspace of b₂ st b₄ /\ b₃ = b₄ holds
b₄ is Subspace of b₃ ) )

proof end;

theorem Th22: :: VECTSP_5:22

proof end;

theorem Th23: :: VECTSP_5:23

proof end;

theorem Th24: :: VECTSP_5:24

proof end;

theorem Th25: :: VECTSP_5:25

proof end;

theorem Th26: :: VECTSP_5:26

canceled;

theorem Th27: :: VECTSP_5:27

proof end;

theorem Th28: :: VECTSP_5:28

Lemma25: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds the carrier of (b₃ /\ b₄) c= the carrier of (b₃ + b₄)

proof end;

theorem Th29: :: VECTSP_5:29

proof end;

Lemma26: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds the carrier of ((b₃ /\ b₄) + b₄) = the carrier of b₄

proof end;

theorem Th30: :: VECTSP_5:30

proof end;

Lemma28: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds the carrier of (b₃ /\ (b₃ + b₄)) = the carrier of b₃

proof end;

theorem Th31: :: VECTSP_5:31

proof end;

Lemma30: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ holds the carrier of ((b₃ /\ b₄) + (b₄ /\ b₅)) c= the carrier of (b₄ /\ (b₃ + b₅))

proof end;

theorem Th32: :: VECTSP_5:32

proof end;

Lemma31: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ is Subspace of b₄ holds
the carrier of (b₄ /\ (b₃ + b₅)) = the carrier of ((b₃ /\ b₄) + (b₄ /\ b₅))

proof end;

theorem Th33: :: VECTSP_5:33

proof end;

Lemma33: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ holds the carrier of (b₃ + (b₄ /\ b₅)) c= the carrier of ((b₄ + b₃) /\ (b₃ + b₅))

proof end;

theorem Th34: :: VECTSP_5:34

proof end;

Lemma34: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄, b₅ being Subspace of b₂ st b₃ is Subspace of b₄ holds
the carrier of (b₄ + (b₃ /\ b₅)) = the carrier of ((b₃ + b₄) /\ (b₄ + b₅))

proof end;

theorem Th35: :: VECTSP_5:35

proof end;

theorem Th36: :: VECTSP_5:36

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being strict Subspace of b₂ st b₅ is Subspace of b₃ holds
b₅ + (b₄ /\ b₃) = (b₅ + b₄) /\ b₃

proof end;

theorem Th37: :: VECTSP_5:37

proof end;

theorem Th38: :: VECTSP_5:38

proof end;

theorem Th39: :: VECTSP_5:39

proof end;

theorem Th40: :: VECTSP_5:40

proof end;

theorem Th41: :: VECTSP_5:41

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds
( ( b₃ is Subspace of b₄ or b₄ is Subspace of b₃ ) iff ex b₅ being Subspace of b₂ st the carrier of b₅ = the carrier of b₃ \/ the carrier of b₄ )

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
func Subspaces c₂ -> set means :Def3: :: VECTSP_5:def 3
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being strict Subspace of a₂ st b₂ = b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Subspaces VECTSP_5:def 3 :

registration

proof end;

end;

theorem Th42: :: VECTSP_5:42

canceled;

theorem Th43: :: VECTSP_5:43

canceled;

theorem Th44: :: VECTSP_5:44

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃, c₄ be Subspace of c₂;
pred c₂ is_the_direct_sum_of c₃,c₄ means :Def4: :: VECTSP_5:def 4
( VectSpStr(# the carrier of a₂,the add of a₂,the Zero of a₂,the lmult of a₂ #) = a₃ + a₄ & a₃ /\ a₄ = (0). a₂ );

end;

:: deftheorem Def4 defines is_the_direct_sum_of VECTSP_5:def 4 :

Lemma38: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ + b₄ = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) iff for b₅ being Element of b₂ ex b₆, b₇ being Element of b₂ st
( b₆ in b₃ & b₇ in b₄ & b₅ = b₆ + b₇ ) )

proof end;

definition

let c₁ be Field;
let c₂ be VectSp of c₁;
let c₃ be Subspace of c₂;
mode Linear_Compl of c₃ -> Subspace of a₂ means :Def5: :: VECTSP_5:def 5
a₂ is_the_direct_sum_of a₄,a₃;
existence

proof end;

end;

:: deftheorem Def5 defines Linear_Compl VECTSP_5:def 5 :

Lemma40: for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
b₂ is_the_direct_sum_of b₄,b₃

proof end;

theorem Th45: :: VECTSP_5:45

canceled;

theorem Th46: :: VECTSP_5:46

canceled;

theorem Th47: :: VECTSP_5:47

for b₁ being Field
for b₂ being VectSp of b₁
for b₃, b₄ being Subspace of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
b₄ is Linear_Compl of b₃

proof end;

theorem Th48: :: VECTSP_5:48

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃ holds
( b₂ is_the_direct_sum_of b₄,b₃ & b₂ is_the_direct_sum_of b₃,b₄ )

proof end;

theorem Th49: :: VECTSP_5:49

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃ holds
( b₃ + b₄ = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) & b₄ + b₃ = VectSpStr(# the carrier of b₂,the add of b₂,the Zero of b₂,the lmult of b₂ #) )

proof end;

theorem Th50: :: VECTSP_5:50

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃ holds
( b₃ /\ b₄ = (0). b₂ & b₄ /\ b₃ = (0). b₂ )

proof end;

theorem Th51: :: VECTSP_5:51

theorem Th52: :: VECTSP_5:52

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁ holds
( b₂ is_the_direct_sum_of (0). b₂, (Omega). b₂ & b₂ is_the_direct_sum_of (Omega). b₂, (0). b₂ )

proof end;

theorem Th53: :: VECTSP_5:53

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃ holds b₃ is Linear_Compl of b₄

proof end;

theorem Th54: :: VECTSP_5:54

for b₁ being Field
for b₂ being VectSp of b₁ holds
( (0). b₂ is Linear_Compl of (Omega). b₂ & (Omega). b₂ is Linear_Compl of (0). b₂ )

proof end;

theorem Th55: :: VECTSP_5:55

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being Coset of b₃
for b₆ being Coset of b₄ st b₅ meets b₆ holds
b₅ /\ b₆ is Coset of b₃ /\ b₄

proof end;

theorem Th56: :: VECTSP_5:56

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₂ is_the_direct_sum_of b₃,b₄ iff for b₅ being Coset of b₃
for b₆ being Coset of b₄ ex b₇ being Element of b₂ st b₅ /\ b₆ = {b₇} )

proof end;

theorem Th57: :: VECTSP_5:57

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable strict VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ holds
( b₃ + b₄ = b₂ iff for b₅ being Element of b₂ ex b₆, b₇ being Element of b₂ st
( b₆ in b₃ & b₇ in b₄ & b₅ = b₆ + b₇ ) ) by Lemma38;

theorem Th58: :: VECTSP_5:58

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅, b₆, b₇, b₈, b₉ being Element of b₂ st b₂ is_the_direct_sum_of b₃,b₄ & b₅ = b₆ + b₇ & b₅ = b₈ + b₉ & b₆ in b₃ & b₈ in b₃ & b₇ in b₄ & b₉ in b₄ holds
( b₆ = b₈ & b₇ = b₉ )

proof end;

theorem Th59: :: VECTSP_5:59

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂ st b₂ = b₃ + b₄ & ex b₅ being Element of b₂ st
for b₆, b₇, b₈, b₉ being Element of b₂ st b₅ = b₆ + b₇ & b₅ = b₈ + b₉ & b₆ in b₃ & b₈ in b₃ & b₇ in b₄ & b₉ in b₄ holds
( b₆ = b₈ & b₇ = b₉ ) holds
b₂ is_the_direct_sum_of b₃,b₄

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
let c₃ be Element of c₂;
let c₄, c₅ be Subspace of c₂;
assume E48: c₂ is_the_direct_sum_of c₄,c₅ ;
func c₃ |-- c₄,c₅ -> Element of [:the carrier of a₂,the carrier of a₂:] means :Def6: :: VECTSP_5:def 6
( a₃ = (a₆ `1 ) + (a₆ `2 ) & a₆ `1 in a₄ & a₆ `2 in a₅ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines |-- VECTSP_5:def 6 :

theorem Th60: :: VECTSP_5:60

canceled;

theorem Th61: :: VECTSP_5:61

canceled;

theorem Th62: :: VECTSP_5:62

canceled;

theorem Th63: :: VECTSP_5:63

canceled;

theorem Th64: :: VECTSP_5:64

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being Element of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
(b₅ |-- b₃,b₄) `1 = (b₅ |-- b₄,b₃) `2

proof end;

theorem Th65: :: VECTSP_5:65

for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr
for b₂ being non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of b₁
for b₃, b₄ being Subspace of b₂
for b₅ being Element of b₂ st b₂ is_the_direct_sum_of b₃,b₄ holds
(b₅ |-- b₃,b₄) `2 = (b₅ |-- b₄,b₃) `1

proof end;

theorem Th66: :: VECTSP_5:66

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃
for b₅ being Element of b₂
for b₆ being Element of [:the carrier of b₂,the carrier of b₂:] st (b₆ `1 ) + (b₆ `2 ) = b₅ & b₆ `1 in b₃ & b₆ `2 in b₄ holds
b₆ = b₅ |-- b₃,b₄

proof end;

theorem Th67: :: VECTSP_5:67

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃
for b₅ being Element of b₂ holds ((b₅ |-- b₃,b₄) `1 ) + ((b₅ |-- b₃,b₄) `2 ) = b₅

proof end;

theorem Th68: :: VECTSP_5:68

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃
for b₅ being Element of b₂ holds
( (b₅ |-- b₃,b₄) `1 in b₃ & (b₅ |-- b₃,b₄) `2 in b₄ )

proof end;

theorem Th69: :: VECTSP_5:69

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃
for b₅ being Element of b₂ holds (b₅ |-- b₃,b₄) `1 = (b₅ |-- b₄,b₃) `2

proof end;

theorem Th70: :: VECTSP_5:70

for b₁ being Field
for b₂ being VectSp of b₁
for b₃ being Subspace of b₂
for b₄ being Linear_Compl of b₃
for b₅ being Element of b₂ holds (b₅ |-- b₃,b₄) `2 = (b₅ |-- b₄,b₃) `1

proof end;

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
func SubJoin c₂ -> BinOp of Subspaces a₂ means :Def7: :: VECTSP_5:def 7
for b₁, b₂ being Element of Subspaces a₂
for b₃, b₄ being Subspace of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ + b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines SubJoin VECTSP_5:def 7 :

definition

let c₁ be non empty Abelian add-associative right_zeroed right_complementable associative distributive left_unital doubleLoopStr ;
let c₂ be non empty Abelian add-associative right_zeroed right_complementable VectSp-like VectSpStr of c₁;
func SubMeet c₂ -> BinOp of Subspaces a₂ means :Def8: :: VECTSP_5:def 8
for b₁, b₂ being Element of Subspaces a₂
for b₃, b₄ being Subspace of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ /\ b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines SubMeet VECTSP_5:def 8 :

theorem Th71: :: VECTSP_5:71

canceled;

theorem Th72: :: VECTSP_5:72

canceled;

theorem Th73: :: VECTSP_5:73

canceled;

theorem Th74: :: VECTSP_5:74

canceled;

theorem Th75: :: VECTSP_5:75

proof end;

theorem Th76: :: VECTSP_5:76

proof end;

theorem Th77: :: VECTSP_5:77

proof end;

theorem Th78: :: VECTSP_5:78

proof end;

theorem Th79: :: VECTSP_5:79

proof end;

theorem Th80: :: VECTSP_5:80

for b₁ being Field
for b₂ being VectSp of b₁ holds LattStr(# (Subspaces b₂),(SubJoin b₂),(SubMeet b₂) #) is C_Lattice

proof end;