:: by Wojciech A. Trybulec

::

:: Received July 27, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

ex b_{1} being strict Subspace of M st the carrier of b_{1} = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) }

for b_{1}, b_{2} being strict Subspace of M st the carrier of b_{1} = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } & the carrier of b_{2} = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } holds

b_{1} = b_{2}
by VECTSP_4:29;

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

func W1 + W2 -> strict Subspace of M means :Def1: :: VECTSP_5:def 1

the carrier of it = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } ;

existence the carrier of it = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines + VECTSP_5:def 1 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for b_{5} being strict Subspace of M holds

( b_{5} = W1 + W2 iff the carrier of b_{5} = { (v + u) where u, v is Element of M : ( v in W1 & u in W2 ) } );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for b

( b

Lm1: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

ex b_{1} being strict Subspace of M st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2

for b_{1}, b_{2} being strict Subspace of M st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2 & the carrier of b_{2} = the carrier of W1 /\ the carrier of W2 holds

b_{1} = b_{2}
by VECTSP_4:29;

commutativity

for b_{1} being strict Subspace of M

for W1, W2 being Subspace of M st the carrier of b_{1} = the carrier of W1 /\ the carrier of W2 holds

the carrier of b_{1} = the carrier of W2 /\ the carrier of W1
;

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

func W1 /\ W2 -> strict Subspace of M means :Def2: :: VECTSP_5:def 2

the carrier of it = the carrier of W1 /\ the carrier of W2;

existence the carrier of it = the carrier of W1 /\ the carrier of W2;

ex b

proof end;

uniqueness for b

b

commutativity

for b

for W1, W2 being Subspace of M st the carrier of b

the carrier of b

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

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for b_{5} being strict Subspace of M holds

( b_{5} = W1 /\ W2 iff the carrier of b_{5} = the carrier of W1 /\ the carrier of W2 );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for b

( b

theorem Th1: :: VECTSP_5:1

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for x being object holds

( x in W1 + W2 iff ex v1, v2 being Element of M st

( v1 in W1 & v2 in W2 & x = v1 + v2 ) )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for x being object holds

( x in W1 + W2 iff ex v1, v2 being Element of M st

( v1 in W1 & v2 in W2 & x = v1 + v2 ) )

proof end;

theorem Th2: :: VECTSP_5:2

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st ( v in W1 or v in W2 ) holds

v in W1 + W2

proof end;

theorem Th3: :: VECTSP_5:3

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for x being object holds

( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for x being object holds

( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )

proof end;

Lm2: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

Lm3: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds

W1 + W2 = W2

proof end;

theorem :: VECTSP_5:4

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds W + W = W by Lm3;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds W + W = W by Lm3;

theorem :: VECTSP_5:5

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by Lm1;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1 by Lm1;

theorem Th6: :: VECTSP_5:6

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3

proof end;

theorem Th7: :: VECTSP_5:7

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )

proof end;

theorem Th8: :: VECTSP_5:8

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2 being strict Subspace of M holds

( W1 is Subspace of W2 iff W1 + W2 = W2 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2 being strict Subspace of M holds

( W1 is Subspace of W2 iff W1 + W2 = W2 )

proof end;

theorem Th9: :: VECTSP_5:9

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds

( ((0). M) + W = W & W + ((0). M) = W )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds

( ((0). M) + W = W & W + ((0). M) = W )

proof end;

Lm4: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9

proof end;

Lm5: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds

( W1 + W = W1 + W9 & W + W1 = W9 + W1 )

proof end;

Lm6: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M holds W is Subspace of (Omega). M

proof end;

theorem :: VECTSP_5:10

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( ((0). M) + ((Omega). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & ((Omega). M) + ((0). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ) by Th9;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( ((0). M) + ((Omega). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & ((Omega). M) + ((0). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ) by Th9;

theorem Th11: :: VECTSP_5:11

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M holds

( ((Omega). M) + W = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M holds

( ((Omega). M) + W = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )

proof end;

theorem :: VECTSP_5:12

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds ((Omega). M) + ((Omega). M) = M by Th11;

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds ((Omega). M) + ((Omega). M) = M by Th11;

theorem :: VECTSP_5:13

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds W /\ W = W

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds W /\ W = W

proof end;

theorem Th14: :: VECTSP_5:14

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3

proof end;

Lm7: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1

proof end;

theorem Th15: :: VECTSP_5:15

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )

proof end;

Lm8: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W, W9, W1 being Subspace of M st the carrier of W = the carrier of W9 holds

( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )

proof end;

theorem Th16: :: VECTSP_5:16

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2 being Subspace of M holds

( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds

W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds

W1 is Subspace of W2 ) )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2 being Subspace of M holds

( ( for W1 being strict Subspace of M st W1 is Subspace of W2 holds

W1 /\ W2 = W1 ) & ( for W1 being Subspace of M st W1 /\ W2 = W1 holds

W1 is Subspace of W2 ) )

proof end;

theorem :: VECTSP_5:17

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W1 /\ W3 is Subspace of W2 /\ W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W1 /\ W3 is Subspace of W2 /\ W3

proof end;

theorem :: VECTSP_5:18

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W3 holds

W1 /\ W2 is Subspace of W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W3 holds

W1 /\ W2 is Subspace of W3

proof end;

theorem :: VECTSP_5:19

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 & W1 is Subspace of W3 holds

W1 is Subspace of W2 /\ W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 & W1 is Subspace of W3 holds

W1 is Subspace of W2 /\ W3

proof end;

theorem Th20: :: VECTSP_5:20

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M holds

( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being Subspace of M holds

( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )

proof end;

theorem Th21: :: VECTSP_5:21

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds

( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W being strict Subspace of M holds

( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )

proof end;

theorem :: VECTSP_5:22

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds ((Omega). M) /\ ((Omega). M) = M by Th21;

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds ((Omega). M) /\ ((Omega). M) = M by Th21;

Lm9: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)

proof end;

theorem :: VECTSP_5:23

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds W1 /\ W2 is Subspace of W1 + W2 by Lm9, VECTSP_4:27;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds W1 /\ W2 is Subspace of W1 + W2 by Lm9, VECTSP_4:27;

Lm10: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2

proof end;

theorem :: VECTSP_5:24

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2 being strict Subspace of M holds (W1 /\ W2) + W2 = W2 by Lm10, VECTSP_4:29;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2 being strict Subspace of M holds (W1 /\ W2) + W2 = W2 by Lm10, VECTSP_4:29;

Lm11: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1

proof end;

theorem :: VECTSP_5:25

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2 being Subspace of M

for W1 being strict Subspace of M holds W1 /\ (W1 + W2) = W1 by Lm11, VECTSP_4:29;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2 being Subspace of M

for W1 being strict Subspace of M holds W1 /\ (W1 + W2) = W1 by Lm11, VECTSP_4:29;

Lm12: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))

proof end;

theorem :: VECTSP_5:26

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm12, VECTSP_4:27;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm12, VECTSP_4:27;

Lm13: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))

proof end;

theorem :: VECTSP_5:27

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm13, VECTSP_4:29;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm13, VECTSP_4:29;

Lm14: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: VECTSP_5:28

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm14, VECTSP_4:27;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm14, VECTSP_4:27;

Lm15: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))

proof end;

theorem :: VECTSP_5:29

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm15, VECTSP_4:29;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm15, VECTSP_4:29;

theorem Th30: :: VECTSP_5:30

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2, W3 being Subspace of M

for W1 being strict Subspace of M st W1 is Subspace of W3 holds

W1 + (W2 /\ W3) = (W1 + W2) /\ W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W2, W3 being Subspace of M

for W1 being strict Subspace of M st W1 is Subspace of W3 holds

W1 + (W2 /\ W3) = (W1 + W2) /\ W3

proof end;

theorem :: VECTSP_5:31

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being strict Subspace of M holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being strict Subspace of M holds

( W1 + W2 = W2 iff W1 /\ W2 = W1 )

proof end;

theorem :: VECTSP_5:32

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds

W1 + W3 is Subspace of W2 + W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1 being Subspace of M

for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds

W1 + W3 is Subspace of W2 + W3

proof end;

theorem :: VECTSP_5:33

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W1 is Subspace of W2 + W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds

W1 is Subspace of W2 + W3

proof end;

theorem :: VECTSP_5:34

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds

W1 + W2 is Subspace of W3

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2, W3 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds

W1 + W2 is Subspace of W3

proof end;

theorem :: VECTSP_5:35

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex W being strict Subspace of M st W = x )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex W being strict Subspace of M st W = x ) ) & ( for x being object holds

( x in b_{2} iff ex W being strict Subspace of M st W = x ) ) holds

b_{1} = b_{2}

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

func Subspaces M -> set means :Def3: :: VECTSP_5:def 3

for x being object holds

( x in it iff ex W being strict Subspace of M st W = x );

existence for x being object holds

( x in it iff ex W being strict Subspace of M st W = x );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Subspaces VECTSP_5:def 3 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b_{3} being set holds

( b_{3} = Subspaces M iff for x being object holds

( x in b_{3} iff ex W being strict Subspace of M st W = x ) );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b

( b

( x in b

registration

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

coherence

not Subspaces M is empty

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

coherence

not Subspaces M is empty

proof end;

theorem :: VECTSP_5:36

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds M in Subspaces M

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds M in Subspaces M

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let W1, W2 be Subspace of M;

:: deftheorem defines is_the_direct_sum_of VECTSP_5:def 4 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( M is_the_direct_sum_of W1,W2 iff ( ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 & W1 /\ W2 = (0). M ) );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( M is_the_direct_sum_of W1,W2 iff ( ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 & W1 /\ W2 = (0). M ) );

Lm16: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 + W2 = ModuleStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) iff for v being Element of M ex v1, v2 being Element of M st

( v1 in W1 & v2 in W2 & v = v1 + v2 ) )

proof end;

definition

let F be Field;

let V be VectSp of F;

let W be Subspace of V;

existence

ex b_{1} being Subspace of V st V is_the_direct_sum_of b_{1},W

end;
let V be VectSp of F;

let W be Subspace of V;

existence

ex b

proof end;

:: deftheorem Def5 defines Linear_Compl VECTSP_5:def 5 :

for F being Field

for V being VectSp of F

for W, b_{4} being Subspace of V holds

( b_{4} is Linear_Compl of W iff V is_the_direct_sum_of b_{4},W );

for F being Field

for V being VectSp of F

for W, b

( b

Lm17: for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds

M is_the_direct_sum_of W2,W1

by Lm1;

theorem :: VECTSP_5:37

for F being Field

for V being VectSp of F

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

W2 is Linear_Compl of W1 by Lm17, Def5;

for V being VectSp of F

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

W2 is Linear_Compl of W1 by Lm17, Def5;

theorem Th38: :: VECTSP_5:38

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) by Def5, Lm17;

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L ) by Def5, Lm17;

theorem Th39: :: VECTSP_5:39

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( W + L = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )

proof end;

theorem Th40: :: VECTSP_5:40

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( W /\ L = (0). V & L /\ W = (0). V )

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds

( W /\ L = (0). V & L /\ W = (0). V )

proof end;

theorem :: VECTSP_5:41

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds

M is_the_direct_sum_of W2,W1 by Lm17;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds

M is_the_direct_sum_of W2,W1 by Lm17;

theorem Th42: :: VECTSP_5:42

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M ) by Th9, Th20;

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds

( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M ) by Th9, Th20;

theorem :: VECTSP_5:43

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds W is Linear_Compl of L

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W holds W is Linear_Compl of L

proof end;

theorem :: VECTSP_5:44

for F being Field

for V being VectSp of F holds

( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Th42, Def5;

for V being VectSp of F holds

( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Th42, Def5;

theorem Th45: :: VECTSP_5:45

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for C1 being Coset of W1

for C2 being Coset of W2 st C1 meets C2 holds

C1 /\ C2 is Coset of W1 /\ W2

proof end;

theorem Th46: :: VECTSP_5:46

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1

for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( M is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1

for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} )

proof end;

theorem :: VECTSP_5:47

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 + W2 = M iff for v being Element of M ex v1, v2 being Element of M st

( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm16;

for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M holds

( W1 + W2 = M iff for v being Element of M ex v1, v2 being Element of M st

( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm16;

theorem Th48: :: VECTSP_5:48

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 )

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v, v1, v2, u1, u2 being Element of M st M is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 )

proof end;

theorem :: VECTSP_5:49

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st

for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

M is_the_direct_sum_of W1,W2

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M st M = W1 + W2 & ex v being Element of M st

for v1, v2, u1, u2 being Element of M st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds

( v1 = u1 & v2 = u2 ) holds

M is_the_direct_sum_of W1,W2

proof end;

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let v be Element of M;

let W1, W2 be Subspace of M;

assume A1: M is_the_direct_sum_of W1,W2 ;

ex b_{1} being Element of [: the carrier of M, the carrier of M:] st

( v = (b_{1} `1) + (b_{1} `2) & b_{1} `1 in W1 & b_{1} `2 in W2 )

for b_{1}, b_{2} being Element of [: the carrier of M, the carrier of M:] st v = (b_{1} `1) + (b_{1} `2) & b_{1} `1 in W1 & b_{1} `2 in W2 & v = (b_{2} `1) + (b_{2} `2) & b_{2} `1 in W1 & b_{2} `2 in W2 holds

b_{1} = b_{2}

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

let v be Element of M;

let W1, W2 be Subspace of M;

assume A1: M is_the_direct_sum_of W1,W2 ;

func v |-- (W1,W2) -> Element of [: the carrier of M, the carrier of M:] means :Def6: :: VECTSP_5:def 6

( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

existence ( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

ex b

( v = (b

proof end;

uniqueness for b

b

proof end;

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

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of M

for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds

for b_{6} being Element of [: the carrier of M, the carrier of M:] holds

( b_{6} = v |-- (W1,W2) iff ( v = (b_{6} `1) + (b_{6} `2) & b_{6} `1 in W1 & b_{6} `2 in W2 ) );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for v being Element of M

for W1, W2 being Subspace of M st M is_the_direct_sum_of W1,W2 holds

for b

( b

theorem Th50: :: VECTSP_5:50

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st M is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st M is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2

proof end;

theorem Th51: :: VECTSP_5:51

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st M is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for W1, W2 being Subspace of M

for v being Element of M st M is_the_direct_sum_of W1,W2 holds

(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1

proof end;

theorem :: VECTSP_5:52

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V

for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds

t = v |-- (W,L)

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V

for t being Element of [: the carrier of V, the carrier of V:] st (t `1) + (t `2) = v & t `1 in W & t `2 in L holds

t = v |-- (W,L)

proof end;

theorem :: VECTSP_5:53

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v

proof end;

theorem :: VECTSP_5:54

for F being Field

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V holds

( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )

for V being VectSp of F

for W being Subspace of V

for L being Linear_Compl of W

for v being Element of V holds

( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )

proof end;

theorem :: VECTSP_5:55

theorem :: VECTSP_5:56

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ex b_{1} being BinOp of (Subspaces M) st

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 + W2

for b_{1}, b_{2} being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{2} . (A1,A2) = W1 + W2 ) holds

b_{1} = b_{2}

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

func SubJoin M -> BinOp of (Subspaces M) means :Def7: :: VECTSP_5:def 7

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 + W2;

existence for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 + W2;

ex b

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

proof end;

uniqueness for b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

b

proof end;

:: deftheorem Def7 defines SubJoin VECTSP_5:def 7 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b_{3} being BinOp of (Subspaces M) holds

( b_{3} = SubJoin M iff for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{3} . (A1,A2) = W1 + W2 );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b

( b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

definition

let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ;

let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

ex b_{1} being BinOp of (Subspaces M) st

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 /\ W2

for b_{1}, b_{2} being BinOp of (Subspaces M) st ( for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{1} . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{2} . (A1,A2) = W1 /\ W2 ) holds

b_{1} = b_{2}

end;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF;

func SubMeet M -> BinOp of (Subspaces M) means :Def8: :: VECTSP_5:def 8

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 /\ W2;

existence for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

it . (A1,A2) = W1 /\ W2;

ex b

for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

proof end;

uniqueness for b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

b

proof end;

:: deftheorem Def8 defines SubMeet VECTSP_5:def 8 :

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b_{3} being BinOp of (Subspaces M) holds

( b_{3} = SubMeet M iff for A1, A2 being Element of Subspaces M

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b_{3} . (A1,A2) = W1 /\ W2 );

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF

for b

( b

for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds

b

theorem Th57: :: VECTSP_5:57

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice

proof end;

theorem Th58: :: VECTSP_5:58

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice

proof end;

theorem Th59: :: VECTSP_5:59

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice

proof end;

theorem Th60: :: VECTSP_5:60

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice

proof end;

theorem :: VECTSP_5:61

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice

for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice

proof end;

theorem :: VECTSP_5:62

for F being Field

for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice

for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice

proof end;