:: VECTSP_5 semantic presentation
begin
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
funcW1 + W2 -> strict Subspace of M means :Def1: :: VECTSP_5:def 1
the carrier of it = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
existence
ex b1 being strict Subspace of M st the carrier of b1 = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
proof
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
set VS = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
{ (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } c= the carrier of M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } or x in the carrier of M )
assume x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ; ::_thesis: x in the carrier of M
then ex v1, v2 being Element of M st
( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
hence x in the carrier of M ; ::_thesis: verum
end;
then reconsider VS = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } as Subset of M ;
A1: 0. M = (0. M) + (0. M) by RLVECT_1:4;
( 0. M in W1 & 0. M in W2 ) by VECTSP_4:17;
then A2: 0. M in VS by A1;
A3: VS = { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) }
proof
thus VS c= { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } c= VS
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VS or x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } )
assume x in VS ; ::_thesis: x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) }
then consider v, u being Element of M such that
A4: x = v + u and
A5: ( v in W1 & u in W2 ) ;
( v in V1 & u in V2 ) by A5, STRUCT_0:def_5;
hence x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } or x in VS )
assume x in { (v + u) where v, u is Element of M : ( v in V1 & u in V2 ) } ; ::_thesis: x in VS
then consider v, u being Element of M such that
A6: x = v + u and
A7: ( v in V1 & u in V2 ) ;
( v in W1 & u in W2 ) by A7, STRUCT_0:def_5;
hence x in VS by A6; ::_thesis: verum
end;
( V1 is linearly-closed & V2 is linearly-closed ) by VECTSP_4:33;
hence ex b1 being strict Subspace of M st the carrier of b1 = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by A2, A3, VECTSP_4:6, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of M st the carrier of b1 = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } & the carrier of b2 = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } holds
b1 = b2 by VECTSP_4:29;
end;
:: deftheorem Def1 defines + VECTSP_5:def_1_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for b5 being strict Subspace of M holds
( b5 = W1 + W2 iff the carrier of b5 = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } );
Lm1: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds W1 + W2 = W2 + W1
let W1, W2 be Subspace of M; ::_thesis: W1 + W2 = W2 + W1
set A = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } ;
A1: { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } c= { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } ; ::_thesis: x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) }
then ex v, u being Element of M st
( x = v + u & v in W2 & u in W1 ) ;
hence x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ; ::_thesis: verum
end;
A2: the carrier of (W1 + W2) = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by Def1;
{ (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } c= { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } or x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ; ::_thesis: x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) }
then ex v, u being Element of M st
( x = v + u & v in W1 & u in W2 ) ;
hence x in { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } ; ::_thesis: verum
end;
then { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } = { (v + u) where v, u is Element of M : ( v in W2 & u in W1 ) } by A1, XBOOLE_0:def_10;
hence W1 + W2 = W2 + W1 by A2, Def1; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
funcW1 /\ W2 -> strict Subspace of M means :Def2: :: VECTSP_5:def 2
the carrier of it = the carrier of W1 /\ the carrier of W2;
existence
ex b1 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2
proof
set VW2 = the carrier of W2;
set VW1 = the carrier of W1;
set VV = the carrier of M;
0. M in W2 by VECTSP_4:17;
then A1: 0. M in the carrier of W2 by STRUCT_0:def_5;
( the carrier of W1 c= the carrier of M & the carrier of W2 c= the carrier of M ) by VECTSP_4:def_2;
then the carrier of W1 /\ the carrier of W2 c= the carrier of M /\ the carrier of M by XBOOLE_1:27;
then reconsider V1 = the carrier of W1, V2 = the carrier of W2, V3 = the carrier of W1 /\ the carrier of W2 as Subset of M by VECTSP_4:def_2;
( V1 is linearly-closed & V2 is linearly-closed ) by VECTSP_4:33;
then A2: V3 is linearly-closed by VECTSP_4:7;
0. M in W1 by VECTSP_4:17;
then 0. M in the carrier of W1 by STRUCT_0:def_5;
then the carrier of W1 /\ the carrier of W2 <> {} by A1, XBOOLE_0:def_4;
hence ex b1 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 by A2, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 & the carrier of b2 = the carrier of W1 /\ the carrier of W2 holds
b1 = b2 by VECTSP_4:29;
commutativity
for b1 being strict Subspace of M
for W1, W2 being Subspace of M st the carrier of b1 = the carrier of W1 /\ the carrier of W2 holds
the carrier of b1 = the carrier of W2 /\ the carrier of W1 ;
end;
:: deftheorem Def2 defines /\ VECTSP_5:def_2_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for b5 being strict Subspace of M holds
( b5 = W1 /\ W2 iff the carrier of b5 = the carrier of W1 /\ the carrier of W2 );
theorem Th1: :: VECTSP_5:1
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let W1, W2 be Subspace of M; ::_thesis: for x being set holds
( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let x be set ; ::_thesis: ( x in W1 + W2 iff ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
thus ( x in W1 + W2 implies ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) ::_thesis: ( ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) implies x in W1 + W2 )
proof
assume x in W1 + W2 ; ::_thesis: ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
then x in the carrier of (W1 + W2) by STRUCT_0:def_5;
then x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by Def1;
then consider v1, v2 being Element of M such that
A1: ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
take v1 ; ::_thesis: ex v2 being Element of M st
( v1 in W1 & v2 in W2 & x = v1 + v2 )
take v2 ; ::_thesis: ( v1 in W1 & v2 in W2 & x = v1 + v2 )
thus ( v1 in W1 & v2 in W2 & x = v1 + v2 ) by A1; ::_thesis: verum
end;
given v1, v2 being Element of M such that A2: ( v1 in W1 & v2 in W2 & x = v1 + v2 ) ; ::_thesis: x in W1 + W2
x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by A2;
then x in the carrier of (W1 + W2) by Def1;
hence x in W1 + W2 by STRUCT_0:def_5; ::_thesis: verum
end;
theorem Th2: :: VECTSP_5:2
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st ( v in W1 or v in W2 ) holds
v in W1 + W2
let v be Element of M; ::_thesis: ( ( v in W1 or v in W2 ) implies v in W1 + W2 )
assume A1: ( v in W1 or v in W2 ) ; ::_thesis: v in W1 + W2
now__::_thesis:_v_in_W1_+_W2
percases ( v in W1 or v in W2 ) by A1;
supposeA2: v in W1 ; ::_thesis: v in W1 + W2
( v = v + (0. M) & 0. M in W2 ) by RLVECT_1:4, VECTSP_4:17;
hence v in W1 + W2 by A2, Th1; ::_thesis: verum
end;
supposeA3: v in W2 ; ::_thesis: v in W1 + W2
( v = (0. M) + v & 0. M in W1 ) by RLVECT_1:4, VECTSP_4:17;
hence v in W1 + W2 by A3, Th1; ::_thesis: verum
end;
end;
end;
hence v in W1 + W2 ; ::_thesis: verum
end;
theorem Th3: :: VECTSP_5:3
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let W1, W2 be Subspace of M; ::_thesis: for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let x be set ; ::_thesis: ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
( x in W1 /\ W2 iff x in the carrier of (W1 /\ W2) ) by STRUCT_0:def_5;
then ( x in W1 /\ W2 iff x in the carrier of W1 /\ the carrier of W2 ) by Def2;
then ( x in W1 /\ W2 iff ( x in the carrier of W1 & x in the carrier of W2 ) ) by XBOOLE_0:def_4;
hence ( x in W1 /\ W2 iff ( x in W1 & x in W2 ) ) by STRUCT_0:def_5; ::_thesis: verum
end;
Lm2: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Subspace of M; ::_thesis: the carrier of W1 c= the carrier of (W1 + W2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 + W2) )
set A = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
assume x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider v = x as Element of W1 ;
reconsider v = v as Element of M by VECTSP_4:10;
A1: v = v + (0. M) by RLVECT_1:4;
( v in W1 & 0. M in W2 ) by STRUCT_0:def_5, VECTSP_4:17;
then x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by A1;
hence x in the carrier of (W1 + W2) by Def1; ::_thesis: verum
end;
Lm3: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1 be Subspace of M; ::_thesis: for W2 being strict Subspace of M st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Subspace of M; ::_thesis: ( the carrier of W1 c= the carrier of W2 implies W1 + W2 = W2 )
assume A1: the carrier of W1 c= the carrier of W2 ; ::_thesis: W1 + W2 = W2
A2: the carrier of (W1 + W2) c= the carrier of W2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 + W2) or x in the carrier of W2 )
assume x in the carrier of (W1 + W2) ; ::_thesis: x in the carrier of W2
then x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by Def1;
then consider v, u being Element of M such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2 ;
W1 is Subspace of W2 by A1, VECTSP_4:27;
then v in W2 by A4, VECTSP_4:8;
then v + u in W2 by A5, VECTSP_4:20;
hence x in the carrier of W2 by A3, STRUCT_0:def_5; ::_thesis: verum
end;
W1 + W2 = W2 + W1 by Lm1;
then the carrier of W2 c= the carrier of (W1 + W2) by Lm2;
then the carrier of (W1 + W2) = the carrier of W2 by A2, XBOOLE_0:def_10;
hence W1 + W2 = W2 by VECTSP_4:29; ::_thesis: verum
end;
theorem :: VECTSP_5:4
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of M; ::_thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } ;
A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } by Def1;
A2: { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } ; ::_thesis: x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) }
then consider v, u being Element of M such that
A3: x = v + u and
A4: v in W1 + W2 and
A5: u in W3 ;
v in the carrier of (W1 + W2) by A4, STRUCT_0:def_5;
then v in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by Def1;
then consider u1, u2 being Element of M such that
A6: v = u1 + u2 and
A7: u1 in W1 and
A8: u2 in W2 ;
u2 + u in { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) } by A5, A8;
then u2 + u in the carrier of (W2 + W3) by Def1;
then A9: u2 + u in W2 + W3 by STRUCT_0:def_5;
v + u = u1 + (u2 + u) by A6, RLVECT_1:def_3;
hence x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; ::_thesis: verum
end;
{ (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } )
assume x in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } ; ::_thesis: x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) }
then consider v, u being Element of M such that
A10: x = v + u and
A11: v in W1 and
A12: u in W2 + W3 ;
u in the carrier of (W2 + W3) by A12, STRUCT_0:def_5;
then u in { (v + u) where v, u is Element of M : ( v in W2 & u in W3 ) } by Def1;
then consider u1, u2 being Element of M such that
A13: u = u1 + u2 and
A14: u1 in W2 and
A15: u2 in W3 ;
v + u1 in { (v + u) where v, u is Element of M : ( v in W1 & u in W2 ) } by A11, A14;
then v + u1 in the carrier of (W1 + W2) by Def1;
then A16: v + u1 in W1 + W2 by STRUCT_0:def_5;
v + u = (v + u1) + u2 by A13, RLVECT_1:def_3;
hence x in { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; ::_thesis: verum
end;
then { (v + u) where v, u is Element of M : ( v in W1 & u in W2 + W3 ) } = { (v + u) where v, u is Element of M : ( v in W1 + W2 & u in W3 ) } by A2, XBOOLE_0:def_10;
hence W1 + (W2 + W3) = (W1 + W2) + W3 by A1, Def1; ::_thesis: verum
end;
theorem Th7: :: VECTSP_5:7
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
let W1, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
the carrier of W1 c= the carrier of (W1 + W2) by Lm2;
hence W1 is Subspace of W1 + W2 by VECTSP_4:27; ::_thesis: W2 is Subspace of W1 + W2
the carrier of W2 c= the carrier of (W2 + W1) by Lm2;
then the carrier of W2 c= the carrier of (W1 + W2) by Lm1;
hence W2 is Subspace of W1 + W2 by VECTSP_4:27; ::_thesis: verum
end;
theorem Th8: :: VECTSP_5:8
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1 being Subspace of M
for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W1 be Subspace of M; ::_thesis: for W2 being strict Subspace of M holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W2 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 iff W1 + W2 = W2 )
thus ( W1 is Subspace of W2 implies W1 + W2 = W2 ) ::_thesis: ( W1 + W2 = W2 implies W1 is Subspace of W2 )
proof
assume W1 is Subspace of W2 ; ::_thesis: W1 + W2 = W2
then the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
hence W1 + W2 = W2 by Lm3; ::_thesis: verum
end;
thus ( W1 + W2 = W2 implies W1 is Subspace of W2 ) by Th7; ::_thesis: verum
end;
theorem Th9: :: VECTSP_5:9
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds
( ((0). M) + W = W & W + ((0). M) = W )
let W be strict Subspace of M; ::_thesis: ( ((0). M) + W = W & W + ((0). M) = W )
(0). M is Subspace of W by VECTSP_4:39;
then the carrier of ((0). M) c= the carrier of W by VECTSP_4:def_2;
hence ((0). M) + W = W by Lm3; ::_thesis: W + ((0). M) = W
hence W + ((0). M) = W by Lm1; ::_thesis: verum
end;
Lm4: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
let W be Subspace of M; ::_thesis: ex W9 being strict Subspace of M st the carrier of W = the carrier of W9
take W9 = W + W; ::_thesis: the carrier of W = the carrier of W9
thus the carrier of W c= the carrier of W9 by Lm2; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W9 c= the carrier of W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W9 or x in the carrier of W )
assume x in the carrier of W9 ; ::_thesis: x in the carrier of W
then x in { (v + u) where v, u is Element of M : ( v in W & u in W ) } by Def1;
then ex v1, v2 being Element of M st
( x = v1 + v2 & v1 in W & v2 in W ) ;
then x in W by VECTSP_4:20;
hence x in the carrier of W by STRUCT_0:def_5; ::_thesis: verum
end;
Lm5: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 )
let W, W9, W1 be Subspace of M; ::_thesis: ( the carrier of W = the carrier of W9 implies ( W1 + W = W1 + W9 & W + W1 = W9 + W1 ) )
assume A1: the carrier of W = the carrier of W9 ; ::_thesis: ( W1 + W = W1 + W9 & W + W1 = W9 + W1 )
A2: now__::_thesis:_for_v_being_Element_of_M_holds_
(_(_v_in_W1_+_W_implies_v_in_W1_+_W9_)_&_(_v_in_W1_+_W9_implies_v_in_W1_+_W_)_)
let v be Element of M; ::_thesis: ( ( v in W1 + W implies v in W1 + W9 ) & ( v in W1 + W9 implies v in W1 + W ) )
set W1W9 = { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 ) } ;
set W1W = { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W ) } ;
thus ( v in W1 + W implies v in W1 + W9 ) ::_thesis: ( v in W1 + W9 implies v in W1 + W )
proof
assume v in W1 + W ; ::_thesis: v in W1 + W9
then v in the carrier of (W1 + W) by STRUCT_0:def_5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W ) } by Def1;
then consider v1, v2 being Element of M such that
A3: ( v = v1 + v2 & v1 in W1 ) and
A4: v2 in W ;
v2 in the carrier of W9 by A1, A4, STRUCT_0:def_5;
then v2 in W9 by STRUCT_0:def_5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 ) } by A3;
then v in the carrier of (W1 + W9) by Def1;
hence v in W1 + W9 by STRUCT_0:def_5; ::_thesis: verum
end;
assume v in W1 + W9 ; ::_thesis: v in W1 + W
then v in the carrier of (W1 + W9) by STRUCT_0:def_5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W9 ) } by Def1;
then consider v1, v2 being Element of M such that
A5: ( v = v1 + v2 & v1 in W1 ) and
A6: v2 in W9 ;
v2 in the carrier of W by A1, A6, STRUCT_0:def_5;
then v2 in W by STRUCT_0:def_5;
then v in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W ) } by A5;
then v in the carrier of (W1 + W) by Def1;
hence v in W1 + W by STRUCT_0:def_5; ::_thesis: verum
end;
hence W1 + W = W1 + W9 by VECTSP_4:30; ::_thesis: W + W1 = W9 + W1
( W1 + W = W + W1 & W1 + W9 = W9 + W1 ) by Lm1;
hence W + W1 = W9 + W1 by A2, VECTSP_4:30; ::_thesis: verum
end;
Lm6: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds W is Subspace of (Omega). M
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds W is Subspace of (Omega). M
let W be Subspace of M; ::_thesis: W is Subspace of (Omega). M
thus the carrier of W c= the carrier of ((Omega). M) by VECTSP_4:def_2; :: according to VECTSP_4:def_2 ::_thesis: ( 0. W = 0. ((Omega). M) & the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus 0. W = 0. M by VECTSP_4:def_2
.= 0. ((Omega). M) by VECTSP_4:def_2 ; ::_thesis: ( the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] )
thus ( the addF of W = K114( the addF of ((Omega). M), the carrier of W) & the lmult of W = the lmult of ((Omega). M) | [: the carrier of GF, the carrier of W:] ) by VECTSP_4:def_2; ::_thesis: verum
end;
theorem :: VECTSP_5:10
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( ((0). M) + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & ((Omega). M) + ((0). M) = VectSpStr(# 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds
( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
let W be Subspace of M; ::_thesis: ( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
consider W9 being strict Subspace of M such that
A1: the carrier of W9 = the carrier of ((Omega). M) ;
A2: the carrier of W c= the carrier of W9 by A1, VECTSP_4:def_2;
A3: W9 is Subspace of (Omega). M by Lm6;
W + ((Omega). M) = W + W9 by A1, Lm5
.= W9 by A2, Lm3
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by A1, A3, VECTSP_4:31 ;
hence ( ((Omega). M) + W = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & W + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ) by Lm1; ::_thesis: verum
end;
theorem :: VECTSP_5:12
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds ((Omega). M) + ((Omega). M) = M by Th11;
theorem :: VECTSP_5:13
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds W /\ W = W
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds W /\ W = W
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds W /\ W = W
let W be strict Subspace of M; ::_thesis: W /\ W = W
the carrier of W = the carrier of W /\ the carrier of W ;
hence W /\ W = W by Def2; ::_thesis: verum
end;
theorem Th14: :: VECTSP_5:14
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let W1, W2, W3 be Subspace of M; ::_thesis: W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
set V1 = the carrier of W1;
set V2 = the carrier of W2;
set V3 = the carrier of W3;
the carrier of (W1 /\ (W2 /\ W3)) = the carrier of W1 /\ the carrier of (W2 /\ W3) by Def2
.= the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) by Def2
.= ( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 by XBOOLE_1:16
.= the carrier of (W1 /\ W2) /\ the carrier of W3 by Def2 ;
hence W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3 by Def2; ::_thesis: verum
end;
Lm7: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of W1
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of W1
the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence the carrier of (W1 /\ W2) c= the carrier of W1 by XBOOLE_1:17; ::_thesis: verum
end;
theorem Th15: :: VECTSP_5:15
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let W1, W2 be Subspace of M; ::_thesis: ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
the carrier of (W1 /\ W2) c= the carrier of W1 by Lm7;
hence W1 /\ W2 is Subspace of W1 by VECTSP_4:27; ::_thesis: W1 /\ W2 is Subspace of W2
the carrier of (W2 /\ W1) c= the carrier of W2 by Lm7;
hence W1 /\ W2 is Subspace of W2 by VECTSP_4:27; ::_thesis: verum
end;
Lm8: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 )
let W, W9, W1 be Subspace of M; ::_thesis: ( the carrier of W = the carrier of W9 implies ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 ) )
assume the carrier of W = the carrier of W9 ; ::_thesis: ( W1 /\ W = W1 /\ W9 & W /\ W1 = W9 /\ W1 )
then A1: the carrier of (W1 /\ W) = the carrier of W1 /\ the carrier of W9 by Def2
.= the carrier of (W1 /\ W9) by Def2 ;
hence W1 /\ W = W1 /\ W9 by VECTSP_4:29; ::_thesis: W /\ W1 = W9 /\ W1
thus W /\ W1 = W9 /\ W1 by A1, VECTSP_4:29; ::_thesis: verum
end;
theorem Th16: :: VECTSP_5:16
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 ) )
let W2 be Subspace of M; ::_thesis: ( ( 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 ) )
thus for W1 being strict Subspace of M st W1 is Subspace of W2 holds
W1 /\ W2 = W1 ::_thesis: for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2
proof
let W1 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W2 = W1 )
assume W1 is Subspace of W2 ; ::_thesis: W1 /\ W2 = W1
then A1: the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence W1 /\ W2 = W1 by A1, VECTSP_4:29, XBOOLE_1:28; ::_thesis: verum
end;
thus for W1 being Subspace of M st W1 /\ W2 = W1 holds
W1 is Subspace of W2 by Th15; ::_thesis: verum
end;
theorem :: VECTSP_5:17
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of (W1 /\ W3);
assume W1 is Subspace of W2 ; ::_thesis: W1 /\ W3 is Subspace of W2 /\ W3
then the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
then the carrier of W1 /\ the carrier of W3 c= the carrier of W2 /\ the carrier of W3 by XBOOLE_1:26;
then the carrier of (W1 /\ W3) c= the carrier of W2 /\ the carrier of W3 by Def2;
then the carrier of (W1 /\ W3) c= the carrier of (W2 /\ W3) by Def2;
hence W1 /\ W3 is Subspace of W2 /\ W3 by VECTSP_4:27; ::_thesis: verum
end;
theorem :: VECTSP_5:18
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
let W1, W3, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W3 implies W1 /\ W2 is Subspace of W3 )
assume A1: W1 is Subspace of W3 ; ::_thesis: W1 /\ W2 is Subspace of W3
W1 /\ W2 is Subspace of W1 by Th15;
hence W1 /\ W2 is Subspace of W3 by A1, VECTSP_4:26; ::_thesis: verum
end;
theorem :: VECTSP_5:19
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 & W1 is Subspace of W3 implies W1 is Subspace of W2 /\ W3 )
assume A1: ( W1 is Subspace of W2 & W1 is Subspace of W3 ) ; ::_thesis: W1 is Subspace of W2 /\ W3
now__::_thesis:_for_v_being_Element_of_M_st_v_in_W1_holds_
v_in_W2_/\_W3
let v be Element of M; ::_thesis: ( v in W1 implies v in W2 /\ W3 )
assume v in W1 ; ::_thesis: v in W2 /\ W3
then ( v in W2 & v in W3 ) by A1, VECTSP_4:8;
hence v in W2 /\ W3 by Th3; ::_thesis: verum
end;
hence W1 is Subspace of W2 /\ W3 by VECTSP_4:28; ::_thesis: verum
end;
theorem Th20: :: VECTSP_5:20
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being Subspace of M holds
( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
let W be Subspace of M; ::_thesis: ( ((0). M) /\ W = (0). M & W /\ ((0). M) = (0). M )
0. M in W by VECTSP_4:17;
then 0. M in the carrier of W by STRUCT_0:def_5;
then {(0. M)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. M)} /\ the carrier of W = {(0. M)} by XBOOLE_1:28;
A2: the carrier of (((0). M) /\ W) = the carrier of ((0). M) /\ the carrier of W by Def2
.= {(0. M)} /\ the carrier of W by VECTSP_4:def_3 ;
hence ((0). M) /\ W = (0). M by A1, VECTSP_4:def_3; ::_thesis: W /\ ((0). M) = (0). M
thus W /\ ((0). M) = (0). M by A2, A1, VECTSP_4:def_3; ::_thesis: verum
end;
theorem Th21: :: VECTSP_5:21
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W being strict Subspace of M holds
( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
let W be strict Subspace of M; ::_thesis: ( ((Omega). M) /\ W = W & W /\ ((Omega). M) = W )
A1: ( the carrier of (((Omega). M) /\ W) = the carrier of VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) /\ the carrier of W & the carrier of W c= the carrier of M ) by Def2, VECTSP_4:def_2;
hence ((Omega). M) /\ W = W by VECTSP_4:29, XBOOLE_1:28; ::_thesis: W /\ ((Omega). M) = W
thus W /\ ((Omega). M) = W by A1, VECTSP_4:29, XBOOLE_1:28; ::_thesis: verum
end;
theorem :: VECTSP_5:22
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds ((Omega). M) /\ ((Omega). M) = M by Th21;
Lm9: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
( the carrier of (W1 /\ W2) c= the carrier of W1 & the carrier of W1 c= the carrier of (W1 + W2) ) by Lm2, Lm7;
hence the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: VECTSP_5:23
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let W1, W2 be Subspace of M; ::_thesis: the carrier of ((W1 /\ W2) + W2) = the carrier of W2
thus the carrier of ((W1 /\ W2) + W2) c= the carrier of W2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + W2) or x in the carrier of W2 )
assume x in the carrier of ((W1 /\ W2) + W2) ; ::_thesis: x in the carrier of W2
then x in { (u + v) where u, v is Element of M : ( u in W1 /\ W2 & v in W2 ) } by Def1;
then consider u, v being Element of M such that
A1: x = u + v and
A2: u in W1 /\ W2 and
A3: v in W2 ;
u in W2 by A2, Th3;
then u + v in W2 by A3, VECTSP_4:20;
hence x in the carrier of W2 by A1, STRUCT_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W2 or x in the carrier of ((W1 /\ W2) + W2) )
the carrier of W2 c= the carrier of (W2 + (W1 /\ W2)) by Lm2;
then A4: the carrier of W2 c= the carrier of ((W1 /\ W2) + W2) by Lm1;
assume x in the carrier of W2 ; ::_thesis: x in the carrier of ((W1 /\ W2) + W2)
hence x in the carrier of ((W1 /\ W2) + W2) by A4; ::_thesis: verum
end;
theorem :: VECTSP_5:24
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Subspace of M; ::_thesis: the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
thus the carrier of (W1 /\ (W1 + W2)) c= the carrier of W1 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of W1 c= the carrier of (W1 /\ (W1 + W2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W1 /\ (W1 + W2)) or x in the carrier of W1 )
assume A1: x in the carrier of (W1 /\ (W1 + W2)) ; ::_thesis: x in the carrier of W1
the carrier of (W1 /\ (W1 + W2)) = the carrier of W1 /\ the carrier of (W1 + W2) by Def2;
hence x in the carrier of W1 by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of W1 or x in the carrier of (W1 /\ (W1 + W2)) )
assume A2: x in the carrier of W1 ; ::_thesis: x in the carrier of (W1 /\ (W1 + W2))
the carrier of W1 c= the carrier of M by VECTSP_4:def_2;
then reconsider x1 = x as Element of M by A2;
A3: ( x1 + (0. M) = x1 & 0. M in W2 ) by RLVECT_1:4, VECTSP_4:17;
x in W1 by A2, STRUCT_0:def_5;
then x in { (u + v) where u, v is Element of M : ( u in W1 & v in W2 ) } by A3;
then x in the carrier of (W1 + W2) by Def1;
then x in the carrier of W1 /\ the carrier of (W1 + W2) by A2, XBOOLE_0:def_4;
hence x in the carrier of (W1 /\ (W1 + W2)) by Def2; ::_thesis: verum
end;
theorem :: VECTSP_5:25
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let W1, W2, W3 be Subspace of M; ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) or x in the carrier of (W2 /\ (W1 + W3)) )
assume x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) ; ::_thesis: x in the carrier of (W2 /\ (W1 + W3))
then x in { (u + v) where u, v is Element of M : ( u in W1 /\ W2 & v in W2 /\ W3 ) } by Def1;
then consider u, v being Element of M such that
A1: x = u + v and
A2: ( u in W1 /\ W2 & v in W2 /\ W3 ) ;
( u in W2 & v in W2 ) by A2, Th3;
then A3: x in W2 by A1, VECTSP_4:20;
( u in W1 & v in W3 ) by A2, Th3;
then x in W1 + W3 by A1, Th1;
then x in W2 /\ (W1 + W3) by A3, Th3;
hence x in the carrier of (W2 /\ (W1 + W3)) by STRUCT_0:def_5; ::_thesis: verum
end;
theorem :: VECTSP_5:26
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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))
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume A1: W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
thus the carrier of (W2 /\ (W1 + W3)) c= the carrier of ((W1 /\ W2) + (W2 /\ W3)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 /\ (W1 + W3)) or x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) )
assume x in the carrier of (W2 /\ (W1 + W3)) ; ::_thesis: x in the carrier of ((W1 /\ W2) + (W2 /\ W3))
then A2: x in the carrier of W2 /\ the carrier of (W1 + W3) by Def2;
then x in the carrier of (W1 + W3) by XBOOLE_0:def_4;
then x in { (u + v) where u, v is Element of M : ( u in W1 & v in W3 ) } by Def1;
then consider u1, v1 being Element of M such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3 ;
A6: u1 in W2 by A1, A4, VECTSP_4:8;
x in the carrier of W2 by A2, XBOOLE_0:def_4;
then u1 + v1 in W2 by A3, STRUCT_0:def_5;
then (v1 + u1) - u1 in W2 by A6, VECTSP_4:23;
then v1 + (u1 - u1) in W2 by RLVECT_1:def_3;
then v1 + (0. M) in W2 by VECTSP_1:19;
then v1 in W2 by RLVECT_1:4;
then A7: v1 in W2 /\ W3 by A5, Th3;
u1 in W1 /\ W2 by A4, A6, Th3;
then x in (W1 /\ W2) + (W2 /\ W3) by A3, A7, Th1;
hence x in the carrier of ((W1 /\ W2) + (W2 /\ W3)) by STRUCT_0:def_5; ::_thesis: verum
end;
thus the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3)) by Lm12; ::_thesis: verum
end;
theorem :: VECTSP_5:27
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W2, W1, W3 being Subspace of M holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let W2, W1, W3 be Subspace of M; ::_thesis: the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (W2 + (W1 /\ W3)) or x in the carrier of ((W1 + W2) /\ (W2 + W3)) )
assume x in the carrier of (W2 + (W1 /\ W3)) ; ::_thesis: x in the carrier of ((W1 + W2) /\ (W2 + W3))
then x in { (u + v) where u, v is Element of M : ( u in W2 & v in W1 /\ W3 ) } by Def1;
then consider u, v being Element of M such that
A1: ( x = u + v & u in W2 ) and
A2: v in W1 /\ W3 ;
v in W3 by A2, Th3;
then x in { (u1 + u2) where u1, u2 is Element of M : ( u1 in W2 & u2 in W3 ) } by A1;
then A3: x in the carrier of (W2 + W3) by Def1;
v in W1 by A2, Th3;
then x in { (v1 + v2) where v1, v2 is Element of M : ( v1 in W1 & v2 in W2 ) } by A1;
then x in the carrier of (W1 + W2) by Def1;
then x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by A3, XBOOLE_0:def_4;
hence x in the carrier of ((W1 + W2) /\ (W2 + W3)) by Def2; ::_thesis: verum
end;
theorem :: VECTSP_5:28
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W2, W1, 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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))
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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))
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3)) )
reconsider V2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
A1: V2 is linearly-closed by VECTSP_4:33;
assume W1 is Subspace of W2 ; ::_thesis: the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
then A2: the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
thus the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm14; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of ((W1 + W2) /\ (W2 + W3)) c= the carrier of (W2 + (W1 /\ W3))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((W1 + W2) /\ (W2 + W3)) or x in the carrier of (W2 + (W1 /\ W3)) )
assume x in the carrier of ((W1 + W2) /\ (W2 + W3)) ; ::_thesis: x in the carrier of (W2 + (W1 /\ W3))
then x in the carrier of (W1 + W2) /\ the carrier of (W2 + W3) by Def2;
then x in the carrier of (W1 + W2) by XBOOLE_0:def_4;
then x in { (u1 + u2) where u1, u2 is Element of M : ( u1 in W1 & u2 in W2 ) } by Def1;
then consider u1, u2 being Element of M such that
A3: x = u1 + u2 and
A4: ( u1 in W1 & u2 in W2 ) ;
( u1 in the carrier of W1 & u2 in the carrier of W2 ) by A4, STRUCT_0:def_5;
then u1 + u2 in V2 by A2, A1, VECTSP_4:def_1;
then A5: u1 + u2 in W2 by STRUCT_0:def_5;
( 0. M in W1 /\ W3 & (u1 + u2) + (0. M) = u1 + u2 ) by RLVECT_1:4, VECTSP_4:17;
then x in { (u + v) where u, v is Element of M : ( u in W2 & v in W1 /\ W3 ) } by A3, A5;
hence x in the carrier of (W2 + (W1 /\ W3)) by Def1; ::_thesis: verum
end;
theorem :: VECTSP_5:29
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W3, W2 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W3, W2 being Subspace of M
for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W3, W2 being Subspace of M
for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W3, W2 be Subspace of M; ::_thesis: for W1 being strict Subspace of M st W1 is Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W1 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3 )
assume A1: W1 is Subspace of W3 ; ::_thesis: W1 + (W2 /\ W3) = (W1 + W2) /\ W3
hence (W1 + W2) /\ W3 = (W1 /\ W3) + (W3 /\ W2) by Lm13, VECTSP_4:29
.= W1 + (W2 /\ W3) by A1, Th16 ;
::_thesis: verum
end;
theorem :: VECTSP_5:31
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being strict Subspace of M holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let W1, W2 be strict Subspace of M; ::_thesis: ( W1 + W2 = W2 iff W1 /\ W2 = W1 )
( W1 + W2 = W2 iff W1 is Subspace of W2 ) by Th8;
hence ( W1 + W2 = W2 iff W1 /\ W2 = W1 ) by Th16; ::_thesis: verum
end;
theorem :: VECTSP_5:32
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1 be Subspace of M; ::_thesis: for W2, W3 being strict Subspace of M st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let W2, W3 be strict Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 + W3 is Subspace of W2 + W3 )
assume A1: W1 is Subspace of W2 ; ::_thesis: W1 + W3 is Subspace of W2 + W3
(W1 + W3) + (W2 + W3) = (W1 + W3) + (W3 + W2) by Lm1
.= ((W1 + W3) + W3) + W2 by Th6
.= (W1 + (W3 + W3)) + W2 by Th6
.= (W1 + W3) + W2 by Lm3
.= W1 + (W3 + W2) by Th6
.= W1 + (W2 + W3) by Lm1
.= (W1 + W2) + W3 by Th6
.= W2 + W3 by A1, Th8 ;
hence W1 + W3 is Subspace of W2 + W3 by Th8; ::_thesis: verum
end;
theorem :: VECTSP_5:33
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
let W1, W2, W3 be Subspace of M; ::_thesis: ( W1 is Subspace of W2 implies W1 is Subspace of W2 + W3 )
assume A1: W1 is Subspace of W2 ; ::_thesis: W1 is Subspace of W2 + W3
W2 is Subspace of W2 + W3 by Th7;
hence W1 is Subspace of W2 + W3 by A1, VECTSP_4:26; ::_thesis: verum
end;
theorem :: VECTSP_5:34
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W3, W2 being Subspace of M st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
let W1, W3, W2 be Subspace of M; ::_thesis: ( W1 is Subspace of W3 & W2 is Subspace of W3 implies W1 + W2 is Subspace of W3 )
assume A1: ( W1 is Subspace of W3 & W2 is Subspace of W3 ) ; ::_thesis: W1 + W2 is Subspace of W3
now__::_thesis:_for_v_being_Element_of_M_st_v_in_W1_+_W2_holds_
v_in_W3
let v be Element of M; ::_thesis: ( v in W1 + W2 implies v in W3 )
assume v in W1 + W2 ; ::_thesis: v in W3
then consider v1, v2 being Element of M such that
A2: ( v1 in W1 & v2 in W2 ) and
A3: v = v1 + v2 by Th1;
( v1 in W3 & v2 in W3 ) by A1, A2, VECTSP_4:8;
hence v in W3 by A3, VECTSP_4:20; ::_thesis: verum
end;
hence W1 + W2 is Subspace of W3 by VECTSP_4:28; ::_thesis: verum
end;
theorem :: VECTSP_5:35
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 )
let W1, W2 be Subspace of M; ::_thesis: ( ( 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 )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
thus ( for W being Subspace of M holds not the carrier of W = the carrier of W1 \/ the carrier of W2 or W1 is Subspace of W2 or W2 is Subspace of W1 ) ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
given W being Subspace of M such that A1: the carrier of W = the carrier of W1 \/ the carrier of W2 ; ::_thesis: ( W1 is Subspace of W2 or W2 is Subspace of W1 )
set VW = the carrier of W;
assume that
A2: W1 is not Subspace of W2 and
A3: W2 is not Subspace of W1 ; ::_thesis: contradiction
not the carrier of W2 c= the carrier of W1 by A3, VECTSP_4:27;
then consider y being set such that
A4: y in the carrier of W2 and
A5: not y in the carrier of W1 by TARSKI:def_3;
reconsider y = y as Element of the carrier of W2 by A4;
reconsider y = y as Element of M by VECTSP_4:10;
reconsider A1 = the carrier of W as Subset of M by VECTSP_4:def_2;
A6: A1 is linearly-closed by VECTSP_4:33;
not the carrier of W1 c= the carrier of W2 by A2, VECTSP_4:27;
then consider x being set such that
A7: x in the carrier of W1 and
A8: not x in the carrier of W2 by TARSKI:def_3;
reconsider x = x as Element of the carrier of W1 by A7;
reconsider x = x as Element of M by VECTSP_4:10;
A9: now__::_thesis:_not_x_+_y_in_the_carrier_of_W2
reconsider A2 = the carrier of W2 as Subset of M by VECTSP_4:def_2;
A10: A2 is linearly-closed by VECTSP_4:33;
assume x + y in the carrier of W2 ; ::_thesis: contradiction
then (x + y) - y in the carrier of W2 by A10, VECTSP_4:3;
then x + (y - y) in the carrier of W2 by RLVECT_1:def_3;
then x + (0. M) in the carrier of W2 by VECTSP_1:19;
hence contradiction by A8, RLVECT_1:4; ::_thesis: verum
end;
A11: now__::_thesis:_not_x_+_y_in_the_carrier_of_W1
reconsider A2 = the carrier of W1 as Subset of M by VECTSP_4:def_2;
A12: A2 is linearly-closed by VECTSP_4:33;
assume x + y in the carrier of W1 ; ::_thesis: contradiction
then (y + x) - x in the carrier of W1 by A12, VECTSP_4:3;
then y + (x - x) in the carrier of W1 by RLVECT_1:def_3;
then y + (0. M) in the carrier of W1 by VECTSP_1:19;
hence contradiction by A5, RLVECT_1:4; ::_thesis: verum
end;
( x in the carrier of W & y in the carrier of W ) by A1, XBOOLE_0:def_3;
then x + y in the carrier of W by A6, VECTSP_4:def_1;
hence contradiction by A1, A11, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
A13: now__::_thesis:_(_W1_is_Subspace_of_W2_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_M_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume W1 is Subspace of W2 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W1 c= the carrier of W2 by VECTSP_4:def_2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W2 by XBOOLE_1:12;
hence ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
A14: now__::_thesis:_(_W2_is_Subspace_of_W1_&_(_W1_is_Subspace_of_W2_or_W2_is_Subspace_of_W1_)_implies_ex_W_being_Subspace_of_M_st_the_carrier_of_W_=_the_carrier_of_W1_\/_the_carrier_of_W2_)
assume W2 is Subspace of W1 ; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W2 c= the carrier of W1 by VECTSP_4:def_2;
then the carrier of W1 \/ the carrier of W2 = the carrier of W1 by XBOOLE_1:12;
hence ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) implies ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 ) ; ::_thesis: verum
end;
assume ( W1 is Subspace of W2 or W2 is Subspace of W1 ) ; ::_thesis: ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2
hence ex W being Subspace of M st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
func Subspaces M -> set means :Def3: :: VECTSP_5:def 3
for x being set holds
( x in it iff ex W being strict Subspace of M st W = x );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x )
proof
defpred S1[ set , set ] means ex W being strict Subspace of M st
( $2 = W & $1 = the carrier of W );
defpred S2[ set ] means ex W being strict Subspace of M st $1 = the carrier of W;
consider B being set such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of M & S2[x] ) ) from XBOOLE_0:sch_1();
A2: for x, y1, y2 being set st S1[x,y1] & S1[x,y2] holds
y1 = y2 by VECTSP_4:29;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch_1(A2);
for x being set holds
( x in B iff ex y being set st [x,y] in f )
proof
let x be set ; ::_thesis: ( x in B iff ex y being set st [x,y] in f )
thus ( x in B implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in B )
proof
assume A4: x in B ; ::_thesis: ex y being set st [x,y] in f
then consider W being strict Subspace of M such that
A5: x = the carrier of W by A1;
reconsider y = W as set ;
take y ; ::_thesis: [x,y] in f
thus [x,y] in f by A3, A4, A5; ::_thesis: verum
end;
given y being set such that A6: [x,y] in f ; ::_thesis: x in B
thus x in B by A3, A6; ::_thesis: verum
end;
then A7: B = dom f by XTUPLE_0:def_12;
for y being set holds
( y in rng f iff ex W being strict Subspace of M st y = W )
proof
let y be set ; ::_thesis: ( y in rng f iff ex W being strict Subspace of M st y = W )
thus ( y in rng f implies ex W being strict Subspace of M st y = W ) ::_thesis: ( ex W being strict Subspace of M st y = W implies y in rng f )
proof
assume y in rng f ; ::_thesis: ex W being strict Subspace of M st y = W
then consider x being set such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
[x,y] in f by A8, FUNCT_1:def_2;
then ex W being strict Subspace of M st
( y = W & x = the carrier of W ) by A3;
hence ex W being strict Subspace of M st y = W ; ::_thesis: verum
end;
given W being strict Subspace of M such that A9: y = W ; ::_thesis: y in rng f
reconsider W = y as Subspace of M by A9;
reconsider x = the carrier of W as set ;
the carrier of W c= the carrier of M by VECTSP_4:def_2;
then A10: x in dom f by A1, A7, A9;
then [x,y] in f by A3, A7, A9;
then y = f . x by A10, FUNCT_1:def_2;
hence y in rng f by A10, FUNCT_1:def_3; ::_thesis: verum
end;
hence ex b1 being set st
for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex W being strict Subspace of M st W = x ) ) & ( for x being set holds
( x in b2 iff ex W being strict Subspace of M st W = x ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff ex W being strict Subspace of M st W = x ) ) & ( for x being set holds
( x in D2 iff ex W being strict Subspace of M st W = x ) ) implies D1 = D2 )
assume A11: for x being set holds
( x in D1 iff ex W being strict Subspace of M st x = W ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies ex W being strict Subspace of M st W = x ) implies ( ex W being strict Subspace of M st W = x & not x in D2 ) ) or D1 = D2 )
assume A12: for x being set holds
( x in D2 iff ex W being strict Subspace of M st x = W ) ; ::_thesis: D1 = D2
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_D1_implies_x_in_D2_)_&_(_x_in_D2_implies_x_in_D1_)_)
let x be set ; ::_thesis: ( ( x in D1 implies x in D2 ) & ( x in D2 implies x in D1 ) )
thus ( x in D1 implies x in D2 ) ::_thesis: ( x in D2 implies x in D1 )
proof
assume x in D1 ; ::_thesis: x in D2
then ex W being strict Subspace of M st x = W by A11;
hence x in D2 by A12; ::_thesis: verum
end;
assume x in D2 ; ::_thesis: x in D1
then ex W being strict Subspace of M st x = W by A12;
hence x in D1 by A11; ::_thesis: verum
end;
hence D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Subspaces VECTSP_5:def_3_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being set holds
( b3 = Subspaces M iff for x being set holds
( x in b3 iff ex W being strict Subspace of M st W = x ) );
registration
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
cluster Subspaces M -> non empty ;
coherence
not Subspaces M is empty
proof
set W = the strict Subspace of M;
the strict Subspace of M in Subspaces M by Def3;
hence not Subspaces M is empty ; ::_thesis: verum
end;
end;
theorem :: VECTSP_5:36
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds M in Subspaces M
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds M in Subspaces M
let M be non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: M in Subspaces M
ex W9 being strict Subspace of M st the carrier of ((Omega). M) = the carrier of W9 ;
hence M in Subspaces M by Def3; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF;
let W1, W2 be Subspace of M;
predM is_the_direct_sum_of W1,W2 means :Def4: :: VECTSP_5:def 4
( VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 & W1 /\ W2 = (0). M );
end;
:: deftheorem Def4 defines is_the_direct_sum_of VECTSP_5:def_4_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( M is_the_direct_sum_of W1,W2 iff ( VectSpStr(# 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# 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 ) )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: for W1, W2 being Subspace of M holds
( W1 + W2 = VectSpStr(# 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 ) )
let W1, W2 be Subspace of M; ::_thesis: ( W1 + W2 = VectSpStr(# 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 ) )
thus ( W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) implies for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) ::_thesis: ( ( for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) implies W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) )
proof
assume A1: W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) ; ::_thesis: for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
let v be Element of M; ::_thesis: ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
v in (Omega). M by RLVECT_1:1;
hence ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) by A1, Th1; ::_thesis: verum
end;
assume A2: for v being Element of M ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ; ::_thesis: W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #)
now__::_thesis:_(_W1_+_W2_is_Subspace_of_(Omega)._M_&_(_for_u_being_Element_of_M_holds_u_in_W1_+_W2_)_)
thus W1 + W2 is Subspace of (Omega). M by Lm6; ::_thesis: for u being Element of M holds u in W1 + W2
let u be Element of M; ::_thesis: u in W1 + W2
ex v1, v2 being Element of M st
( v1 in W1 & v2 in W2 & u = v1 + v2 ) by A2;
hence u in W1 + W2 by Th1; ::_thesis: verum
end;
hence W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by VECTSP_4:32; ::_thesis: verum
end;
definition
let F be Field;
let V be VectSp of F;
let W be Subspace of V;
mode Linear_Compl of W -> Subspace of V means :Def5: :: VECTSP_5:def 5
V is_the_direct_sum_of it,W;
existence
ex b1 being Subspace of V st V is_the_direct_sum_of b1,W
proof
defpred S1[ set , set ] means ex W1, W2 being strict Subspace of V st
( $1 = W1 & $2 = W2 & W1 is Subspace of W2 );
defpred S2[ set ] means ex W1 being strict Subspace of V st
( $1 = W1 & W /\ W1 = (0). V );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Subspaces V & S2[x] ) ) from XBOOLE_0:sch_1();
( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by Def3, Th20;
then reconsider X = X as non empty set by A1;
consider R being Relation of X such that
A2: for x, y being Element of X holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
defpred S3[ set , set ] means [$1,$2] in R;
A3: now__::_thesis:_for_x,_y_being_Element_of_X_st_S3[x,y]_&_S3[y,x]_holds_
x_=_y
let x, y be Element of X; ::_thesis: ( S3[x,y] & S3[y,x] implies x = y )
assume ( S3[x,y] & S3[y,x] ) ; ::_thesis: x = y
then ( ex W1, W2 being strict Subspace of V st
( x = W1 & y = W2 & W1 is Subspace of W2 ) & ex W3, W4 being strict Subspace of V st
( y = W3 & x = W4 & W3 is Subspace of W4 ) ) by A2;
hence x = y by VECTSP_4:25; ::_thesis: verum
end;
A4: for Y being set st Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S3[x,y] holds
S3[y,x] ) holds
ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y]
proof
let Y be set ; ::_thesis: ( Y c= X & ( for x, y being Element of X st x in Y & y in Y & not S3[x,y] holds
S3[y,x] ) implies ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y] )
assume that
A5: Y c= X and
A6: for x, y being Element of X st x in Y & y in Y & not [x,y] in R holds
[y,x] in R ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y]
now__::_thesis:_ex_y9_being_Element_of_X_st_
for_x_being_Element_of_X_st_x_in_Y_holds_
[x,y9]_in_R
percases ( Y = {} or Y <> {} ) ;
supposeA7: Y = {} ; ::_thesis: ex y9 being Element of X st
for x being Element of X st x in Y holds
[x,y9] in R
set y = the Element of X;
take y9 = the Element of X; ::_thesis: for x being Element of X st x in Y holds
[x,y9] in R
let x be Element of X; ::_thesis: ( x in Y implies [x,y9] in R )
assume x in Y ; ::_thesis: [x,y9] in R
hence [x,y9] in R by A7; ::_thesis: verum
end;
supposeA8: Y <> {} ; ::_thesis: ex y being Element of X st
for x being Element of X st x in Y holds
[x,y] in R
defpred S4[ set , set ] means ex W1 being strict Subspace of V st
( $1 = W1 & $2 = the carrier of W1 );
A9: for x being set st x in Y holds
ex y being set st S4[x,y]
proof
let x be set ; ::_thesis: ( x in Y implies ex y being set st S4[x,y] )
assume x in Y ; ::_thesis: ex y being set st S4[x,y]
then consider W1 being strict Subspace of V such that
A10: x = W1 and
W /\ W1 = (0). V by A1, A5;
reconsider y = the carrier of W1 as set ;
take y ; ::_thesis: S4[x,y]
take W1 ; ::_thesis: ( x = W1 & y = the carrier of W1 )
thus ( x = W1 & y = the carrier of W1 ) by A10; ::_thesis: verum
end;
consider f being Function such that
A11: dom f = Y and
A12: for x being set st x in Y holds
S4[x,f . x] from CLASSES1:sch_1(A9);
set Z = union (rng f);
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_f)_holds_
x_in_the_carrier_of_V
let x be set ; ::_thesis: ( x in union (rng f) implies x in the carrier of V )
assume x in union (rng f) ; ::_thesis: x in the carrier of V
then consider Y9 being set such that
A13: x in Y9 and
A14: Y9 in rng f by TARSKI:def_4;
consider y being set such that
A15: y in dom f and
A16: f . y = Y9 by A14, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
y = W1 and
A17: f . y = the carrier of W1 by A11, A12, A15;
the carrier of W1 c= the carrier of V by VECTSP_4:def_2;
hence x in the carrier of V by A13, A16, A17; ::_thesis: verum
end;
then reconsider Z = union (rng f) as Subset of V by TARSKI:def_3;
A18: Z is linearly-closed
proof
thus for v1, v2 being Element of V st v1 in Z & v2 in Z holds
v1 + v2 in Z :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of F
for b2 being Element of the carrier of V holds
( not b2 in Z or b1 * b2 in Z )
proof
let v1, v2 be Element of V; ::_thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that
A19: v1 in Z and
A20: v2 in Z ; ::_thesis: v1 + v2 in Z
consider Y1 being set such that
A21: v1 in Y1 and
A22: Y1 in rng f by A19, TARSKI:def_4;
consider y1 being set such that
A23: y1 in dom f and
A24: f . y1 = Y1 by A22, FUNCT_1:def_3;
consider Y2 being set such that
A25: v2 in Y2 and
A26: Y2 in rng f by A20, TARSKI:def_4;
consider y2 being set such that
A27: y2 in dom f and
A28: f . y2 = Y2 by A26, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
A29: y1 = W1 and
A30: f . y1 = the carrier of W1 by A11, A12, A23;
consider W2 being strict Subspace of V such that
A31: y2 = W2 and
A32: f . y2 = the carrier of W2 by A11, A12, A27;
reconsider y1 = y1, y2 = y2 as Element of X by A5, A11, A23, A27;
now__::_thesis:_v1_+_v2_in_Z
percases ( [y1,y2] in R or [y2,y1] in R ) by A6, A11, A23, A27;
suppose [y1,y2] in R ; ::_thesis: v1 + v2 in Z
then ex W3, W4 being strict Subspace of V st
( y1 = W3 & y2 = W4 & W3 is Subspace of W4 ) by A2;
then the carrier of W1 c= the carrier of W2 by A29, A31, VECTSP_4:def_2;
then A33: v1 in W2 by A21, A24, A30, STRUCT_0:def_5;
v2 in W2 by A25, A28, A32, STRUCT_0:def_5;
then v1 + v2 in W2 by A33, VECTSP_4:20;
then A34: v1 + v2 in the carrier of W2 by STRUCT_0:def_5;
f . y2 in rng f by A27, FUNCT_1:def_3;
hence v1 + v2 in Z by A32, A34, TARSKI:def_4; ::_thesis: verum
end;
suppose [y2,y1] in R ; ::_thesis: v1 + v2 in Z
then ex W3, W4 being strict Subspace of V st
( y2 = W3 & y1 = W4 & W3 is Subspace of W4 ) by A2;
then the carrier of W2 c= the carrier of W1 by A29, A31, VECTSP_4:def_2;
then A35: v2 in W1 by A25, A28, A32, STRUCT_0:def_5;
v1 in W1 by A21, A24, A30, STRUCT_0:def_5;
then v1 + v2 in W1 by A35, VECTSP_4:20;
then A36: v1 + v2 in the carrier of W1 by STRUCT_0:def_5;
f . y1 in rng f by A23, FUNCT_1:def_3;
hence v1 + v2 in Z by A30, A36, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence v1 + v2 in Z ; ::_thesis: verum
end;
let a be Element of F; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in Z or a * b1 in Z )
let v1 be Element of V; ::_thesis: ( not v1 in Z or a * v1 in Z )
assume v1 in Z ; ::_thesis: a * v1 in Z
then consider Y1 being set such that
A37: v1 in Y1 and
A38: Y1 in rng f by TARSKI:def_4;
consider y1 being set such that
A39: y1 in dom f and
A40: f . y1 = Y1 by A38, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
y1 = W1 and
A41: f . y1 = the carrier of W1 by A11, A12, A39;
v1 in W1 by A37, A40, A41, STRUCT_0:def_5;
then a * v1 in W1 by VECTSP_4:21;
then A42: a * v1 in the carrier of W1 by STRUCT_0:def_5;
f . y1 in rng f by A39, FUNCT_1:def_3;
hence a * v1 in Z by A41, A42, TARSKI:def_4; ::_thesis: verum
end;
set z = the Element of rng f;
A43: rng f <> {} by A8, A11, RELAT_1:42;
then consider z1 being set such that
A44: z1 in dom f and
A45: f . z1 = the Element of rng f by FUNCT_1:def_3;
ex W3 being strict Subspace of V st
( z1 = W3 & f . z1 = the carrier of W3 ) by A11, A12, A44;
then Z <> {} by A43, A45, ORDERS_1:6;
then consider E being strict Subspace of V such that
A46: Z = the carrier of E by A18, VECTSP_4:34;
now__::_thesis:_for_u_being_Element_of_V_holds_
(_(_u_in_W_/\_E_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_W_/\_E_)_)
let u be Element of V; ::_thesis: ( ( u in W /\ E implies u in (0). V ) & ( u in (0). V implies u in W /\ E ) )
thus ( u in W /\ E implies u in (0). V ) ::_thesis: ( u in (0). V implies u in W /\ E )
proof
assume A47: u in W /\ E ; ::_thesis: u in (0). V
then A48: u in W by Th3;
u in E by A47, Th3;
then u in Z by A46, STRUCT_0:def_5;
then consider Y1 being set such that
A49: u in Y1 and
A50: Y1 in rng f by TARSKI:def_4;
consider y1 being set such that
A51: y1 in dom f and
A52: f . y1 = Y1 by A50, FUNCT_1:def_3;
A53: ex W2 being strict Subspace of V st
( y1 = W2 & W /\ W2 = (0). V ) by A1, A5, A11, A51;
consider W1 being strict Subspace of V such that
A54: y1 = W1 and
A55: f . y1 = the carrier of W1 by A11, A12, A51;
u in W1 by A49, A52, A55, STRUCT_0:def_5;
hence u in (0). V by A54, A48, A53, Th3; ::_thesis: verum
end;
assume u in (0). V ; ::_thesis: u in W /\ E
then u in the carrier of ((0). V) by STRUCT_0:def_5;
then u in {(0. V)} by VECTSP_4:def_3;
then u = 0. V by TARSKI:def_1;
hence u in W /\ E by VECTSP_4:17; ::_thesis: verum
end;
then A56: W /\ E = (0). V by VECTSP_4:30;
E in Subspaces V by Def3;
then reconsider y9 = E as Element of X by A1, A56;
take y = y9; ::_thesis: for x being Element of X st x in Y holds
[x,y] in R
let x be Element of X; ::_thesis: ( x in Y implies [x,y] in R )
assume A57: x in Y ; ::_thesis: [x,y] in R
then consider W1 being strict Subspace of V such that
A58: x = W1 and
A59: f . x = the carrier of W1 by A12;
now__::_thesis:_for_u_being_Element_of_V_st_u_in_W1_holds_
u_in_E
let u be Element of V; ::_thesis: ( u in W1 implies u in E )
assume u in W1 ; ::_thesis: u in E
then A60: u in the carrier of W1 by STRUCT_0:def_5;
the carrier of W1 in rng f by A11, A57, A59, FUNCT_1:def_3;
then u in Z by A60, TARSKI:def_4;
hence u in E by A46, STRUCT_0:def_5; ::_thesis: verum
end;
then W1 is Subspace of E by VECTSP_4:28;
hence [x,y] in R by A2, A58; ::_thesis: verum
end;
end;
end;
hence ex y being Element of X st
for x being Element of X st x in Y holds
S3[x,y] ; ::_thesis: verum
end;
A61: now__::_thesis:_for_x,_y,_z_being_Element_of_X_st_S3[x,y]_&_S3[y,z]_holds_
S3[x,z]
let x, y, z be Element of X; ::_thesis: ( S3[x,y] & S3[y,z] implies S3[x,z] )
assume that
A62: S3[x,y] and
A63: S3[y,z] ; ::_thesis: S3[x,z]
consider W1, W2 being strict Subspace of V such that
A64: x = W1 and
A65: ( y = W2 & W1 is Subspace of W2 ) by A2, A62;
consider W3, W4 being strict Subspace of V such that
A66: y = W3 and
A67: z = W4 and
A68: W3 is Subspace of W4 by A2, A63;
W1 is Subspace of W4 by A65, A66, A68, VECTSP_4:26;
hence S3[x,z] by A2, A64, A67; ::_thesis: verum
end;
A69: now__::_thesis:_for_x_being_Element_of_X_holds_S3[x,x]
let x be Element of X; ::_thesis: S3[x,x]
consider W1 being strict Subspace of V such that
A70: x = W1 and
W /\ W1 = (0). V by A1;
W1 is Subspace of W1 by VECTSP_4:24;
hence S3[x,x] by A2, A70; ::_thesis: verum
end;
consider x being Element of X such that
A71: for y being Element of X st x <> y holds
not S3[x,y] from ORDERS_1:sch_1(A69, A3, A61, A4);
consider L being strict Subspace of V such that
A72: x = L and
A73: W /\ L = (0). V by A1;
take L ; ::_thesis: V is_the_direct_sum_of L,W
thus VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W :: according to VECTSP_5:def_4 ::_thesis: L /\ W = (0). V
proof
assume not VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = L + W ; ::_thesis: contradiction
then consider v being Element of V such that
A74: for v1, v2 being Element of V holds
( not v1 in L or not v2 in W or v <> v1 + v2 ) by Lm16;
( v = (0. V) + v & 0. V in W ) by RLVECT_1:4, VECTSP_4:17;
then A75: not v in L by A74;
set A = { (a * v) where a is Element of F : verum } ;
A76: (1_ F) * v in { (a * v) where a is Element of F : verum } ;
now__::_thesis:_for_x_being_set_st_x_in__{__(a_*_v)_where_a_is_Element_of_F_:_verum__}__holds_
x_in_the_carrier_of_V
let x be set ; ::_thesis: ( x in { (a * v) where a is Element of F : verum } implies x in the carrier of V )
assume x in { (a * v) where a is Element of F : verum } ; ::_thesis: x in the carrier of V
then ex a being Element of F st x = a * v ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider A = { (a * v) where a is Element of F : verum } as Subset of V by TARSKI:def_3;
A is linearly-closed
proof
thus for v1, v2 being Element of V st v1 in A & v2 in A holds
v1 + v2 in A :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of F
for b2 being Element of the carrier of V holds
( not b2 in A or b1 * b2 in A )
proof
let v1, v2 be Element of V; ::_thesis: ( v1 in A & v2 in A implies v1 + v2 in A )
assume v1 in A ; ::_thesis: ( not v2 in A or v1 + v2 in A )
then consider a1 being Element of F such that
A77: v1 = a1 * v ;
assume v2 in A ; ::_thesis: v1 + v2 in A
then consider a2 being Element of F such that
A78: v2 = a2 * v ;
v1 + v2 = (a1 + a2) * v by A77, A78, VECTSP_1:def_15;
hence v1 + v2 in A ; ::_thesis: verum
end;
let a be Element of F; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A or a * b1 in A )
let v1 be Element of V; ::_thesis: ( not v1 in A or a * v1 in A )
assume v1 in A ; ::_thesis: a * v1 in A
then consider a1 being Element of F such that
A79: v1 = a1 * v ;
a * v1 = (a * a1) * v by A79, VECTSP_1:def_16;
hence a * v1 in A ; ::_thesis: verum
end;
then consider Z being strict Subspace of V such that
A80: the carrier of Z = A by A76, VECTSP_4:34;
A81: not v in L + W by A74, Th1;
now__::_thesis:_for_u_being_Element_of_V_holds_
(_(_u_in_Z_/\_(W_+_L)_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_Z_/\_(W_+_L)_)_)
let u be Element of V; ::_thesis: ( ( u in Z /\ (W + L) implies u in (0). V ) & ( u in (0). V implies u in Z /\ (W + L) ) )
thus ( u in Z /\ (W + L) implies u in (0). V ) ::_thesis: ( u in (0). V implies u in Z /\ (W + L) )
proof
assume A82: u in Z /\ (W + L) ; ::_thesis: u in (0). V
then u in Z by Th3;
then u in A by A80, STRUCT_0:def_5;
then consider a being Element of F such that
A83: u = a * v ;
now__::_thesis:_not_a_<>_0._F
u in W + L by A82, Th3;
then (a ") * (a * v) in W + L by A83, VECTSP_4:21;
then A84: ((a ") * a) * v in W + L by VECTSP_1:def_16;
assume a <> 0. F ; ::_thesis: contradiction
then (1_ F) * v in W + L by A84, VECTSP_1:def_10;
then (1_ F) * v in L + W by Lm1;
hence contradiction by A81, VECTSP_1:def_17; ::_thesis: verum
end;
then u = 0. V by A83, VECTSP_1:14;
hence u in (0). V by VECTSP_4:17; ::_thesis: verum
end;
assume u in (0). V ; ::_thesis: u in Z /\ (W + L)
then u in the carrier of ((0). V) by STRUCT_0:def_5;
then u in {(0. V)} by VECTSP_4:def_3;
then u = 0. V by TARSKI:def_1;
hence u in Z /\ (W + L) by VECTSP_4:17; ::_thesis: verum
end;
then A85: Z /\ (W + L) = (0). V by VECTSP_4:30;
now__::_thesis:_for_u_being_Element_of_V_holds_
(_(_u_in_(Z_+_L)_/\_W_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_(Z_+_L)_/\_W_)_)
let u be Element of V; ::_thesis: ( ( u in (Z + L) /\ W implies u in (0). V ) & ( u in (0). V implies u in (Z + L) /\ W ) )
thus ( u in (Z + L) /\ W implies u in (0). V ) ::_thesis: ( u in (0). V implies u in (Z + L) /\ W )
proof
assume A86: u in (Z + L) /\ W ; ::_thesis: u in (0). V
then u in Z + L by Th3;
then consider v1, v2 being Element of V such that
A87: v1 in Z and
A88: v2 in L and
A89: u = v1 + v2 by Th1;
A90: u in W by A86, Th3;
then A91: u in W + L by Th2;
( v1 = u - v2 & v2 in W + L ) by A88, A89, Th2, VECTSP_2:2;
then v1 in W + L by A91, VECTSP_4:23;
then v1 in Z /\ (W + L) by A87, Th3;
then v1 in the carrier of ((0). V) by A85, STRUCT_0:def_5;
then v1 in {(0. V)} by VECTSP_4:def_3;
then v1 = 0. V by TARSKI:def_1;
then v2 = u by A89, RLVECT_1:4;
hence u in (0). V by A73, A88, A90, Th3; ::_thesis: verum
end;
assume u in (0). V ; ::_thesis: u in (Z + L) /\ W
then u in the carrier of ((0). V) by STRUCT_0:def_5;
then u in {(0. V)} by VECTSP_4:def_3;
then u = 0. V by TARSKI:def_1;
hence u in (Z + L) /\ W by VECTSP_4:17; ::_thesis: verum
end;
then A92: W /\ (Z + L) = (0). V by VECTSP_4:30;
Z + L in Subspaces V by Def3;
then reconsider x1 = Z + L as Element of X by A1, A92;
L is Subspace of Z + L by Th7;
then A93: [x,x1] in R by A2, A72;
v in A by A76, VECTSP_1:def_17;
then v in Z by A80, STRUCT_0:def_5;
then Z + L <> L by A75, Th2;
hence contradiction by A71, A72, A93; ::_thesis: verum
end;
thus L /\ W = (0). V by A73; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Linear_Compl VECTSP_5:def_5_:_
for F being Field
for V being VectSp of F
for W, b4 being Subspace of V holds
( b4 is Linear_Compl of W iff V is_the_direct_sum_of b4,W );
Lm17: for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies M is_the_direct_sum_of W2,W1 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: M is_the_direct_sum_of W2,W1
then VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by Def4;
then A2: VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W2 + W1 by Lm1;
W2 /\ W1 = (0). M by A1, Def4;
hence M is_the_direct_sum_of W2,W1 by A2, Def4; ::_thesis: verum
end;
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
proof
let F be Field; ::_thesis: 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
let V be VectSp of F; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
W2 is Linear_Compl of W1
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies W2 is Linear_Compl of W1 )
assume V is_the_direct_sum_of W1,W2 ; ::_thesis: W2 is Linear_Compl of W1
then V is_the_direct_sum_of W2,W1 by Lm17;
hence W2 is Linear_Compl of W1 by Def5; ::_thesis: verum
end;
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 )
proof
let F be Field; ::_thesis: 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 )
let V be VectSp of F; ::_thesis: 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 )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
let L be Linear_Compl of W; ::_thesis: ( V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L )
thus V is_the_direct_sum_of L,W by Def5; ::_thesis: V is_the_direct_sum_of W,L
hence V is_the_direct_sum_of W,L by Lm17; ::_thesis: verum
end;
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 = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
proof
let F be Field; ::_thesis: for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
let L be Linear_Compl of W; ::_thesis: ( W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) & L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) )
V is_the_direct_sum_of W,L by Th38;
hence W + L = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Def4; ::_thesis: L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
hence L + W = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Lm1; ::_thesis: verum
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 )
proof
let F be Field; ::_thesis: 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 )
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
let L be Linear_Compl of W; ::_thesis: ( W /\ L = (0). V & L /\ W = (0). V )
A1: V is_the_direct_sum_of W,L by Th38;
hence W /\ L = (0). V by Def4; ::_thesis: L /\ W = (0). V
thus L /\ W = (0). V by A1, Def4; ::_thesis: verum
end;
theorem :: VECTSP_5:41
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds
( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: ( M is_the_direct_sum_of (0). M, (Omega). M & M is_the_direct_sum_of (Omega). M, (0). M )
( ((0). M) + ((Omega). M) = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) & (0). M = ((0). M) /\ ((Omega). M) ) by Th9, Th20;
hence M is_the_direct_sum_of (0). M, (Omega). M by Def4; ::_thesis: M is_the_direct_sum_of (Omega). M, (0). M
hence M is_the_direct_sum_of (Omega). M, (0). M by Lm17; ::_thesis: verum
end;
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
proof
let F be Field; ::_thesis: 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
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds W is Linear_Compl of L
let L be Linear_Compl of W; ::_thesis: W is Linear_Compl of L
V is_the_direct_sum_of L,W by Def5;
then V is_the_direct_sum_of W,L by Lm17;
hence W is Linear_Compl of L by Def5; ::_thesis: verum
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 )
proof
let F be Field; ::_thesis: for V being VectSp of F holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
let V be VectSp of F; ::_thesis: ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th42;
hence ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def5; ::_thesis: verum
end;
theorem Th45: :: VECTSP_5:45
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 st C1 meets C2 holds
C1 /\ C2 is Coset of W1 /\ W2
let C2 be Coset of W2; ::_thesis: ( C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2 )
set v = the Element of C1 /\ C2;
set C = C1 /\ C2;
assume A1: C1 /\ C2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: C1 /\ C2 is Coset of W1 /\ W2
then reconsider v = the Element of C1 /\ C2 as Element of M by TARSKI:def_3;
v in C2 by A1, XBOOLE_0:def_4;
then A2: C2 = v + W2 by VECTSP_4:77;
v in C1 by A1, XBOOLE_0:def_4;
then A3: C1 = v + W1 by VECTSP_4:77;
C1 /\ C2 is Coset of W1 /\ W2
proof
take v ; :: according to VECTSP_4:def_6 ::_thesis: C1 /\ C2 = v + (W1 /\ W2)
thus C1 /\ C2 c= v + (W1 /\ W2) :: according to XBOOLE_0:def_10 ::_thesis: v + (W1 /\ W2) c= C1 /\ C2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )
assume A4: x in C1 /\ C2 ; ::_thesis: x in v + (W1 /\ W2)
then x in C1 by XBOOLE_0:def_4;
then consider u1 being Element of M such that
A5: u1 in W1 and
A6: x = v + u1 by A3, VECTSP_4:42;
x in C2 by A4, XBOOLE_0:def_4;
then consider u2 being Element of M such that
A7: u2 in W2 and
A8: x = v + u2 by A2, VECTSP_4:42;
u1 = u2 by A6, A8, RLVECT_1:8;
then u1 in W1 /\ W2 by A5, A7, Th3;
hence x in v + (W1 /\ W2) by A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in v + (W1 /\ W2) or x in C1 /\ C2 )
assume x in v + (W1 /\ W2) ; ::_thesis: x in C1 /\ C2
then consider u being Element of M such that
A9: u in W1 /\ W2 and
A10: x = v + u by VECTSP_4:42;
u in W2 by A9, Th3;
then A11: x in { (v + u2) where u2 is Element of M : u2 in W2 } by A10;
u in W1 by A9, Th3;
then x in { (v + u1) where u1 is Element of M : u1 in W1 } by A10;
hence x in C1 /\ C2 by A3, A2, A11, XBOOLE_0:def_4; ::_thesis: verum
end;
hence C1 /\ C2 is Coset of W1 /\ W2 ; ::_thesis: verum
end;
theorem Th46: :: VECTSP_5:46
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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} )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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} )
let W1, W2 be Subspace of M; ::_thesis: ( 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} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
A1: W1 + W2 is Subspace of (Omega). M by Lm6;
thus ( M is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ) ::_thesis: ( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ) implies M is_the_direct_sum_of W1,W2 )
proof
assume A2: M is_the_direct_sum_of W1,W2 ; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
then A3: VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by Def4;
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v}
let C2 be Coset of W2; ::_thesis: ex v being Element of M st C1 /\ C2 = {v}
consider v1 being Element of M such that
A4: C1 = v1 + W1 by VECTSP_4:def_6;
v1 in (Omega). M by RLVECT_1:1;
then consider v11, v12 being Element of M such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3, Th1;
consider v2 being Element of M such that
A8: C2 = v2 + W2 by VECTSP_4:def_6;
v2 in (Omega). M by RLVECT_1:1;
then consider v21, v22 being Element of M such that
A9: v21 in W1 and
A10: v22 in W2 and
A11: v2 = v21 + v22 by A3, Th1;
take v = v12 + v21; ::_thesis: C1 /\ C2 = {v}
{v} = C1 /\ C2
proof
thus A12: {v} c= C1 /\ C2 :: according to XBOOLE_0:def_10 ::_thesis: C1 /\ C2 c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in C1 /\ C2 )
assume x in {v} ; ::_thesis: x in C1 /\ C2
then A13: x = v by TARSKI:def_1;
v21 = v2 - v22 by A11, VECTSP_2:2;
then v21 in C2 by A8, A10, VECTSP_4:62;
then C2 = v21 + W2 by VECTSP_4:77;
then A14: x in C2 by A6, A13;
v12 = v1 - v11 by A7, VECTSP_2:2;
then v12 in C1 by A4, A5, VECTSP_4:62;
then C1 = v12 + W1 by VECTSP_4:77;
then x in C1 by A9, A13;
hence x in C1 /\ C2 by A14, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in {v} )
assume A15: x in C1 /\ C2 ; ::_thesis: x in {v}
then C1 meets C2 by XBOOLE_0:4;
then reconsider C = C1 /\ C2 as Coset of W1 /\ W2 by Th45;
A16: v in {v} by TARSKI:def_1;
W1 /\ W2 = (0). M by A2, Def4;
then ex u being Element of M st C = {u} by VECTSP_4:72;
hence x in {v} by A12, A15, A16, TARSKI:def_1; ::_thesis: verum
end;
hence C1 /\ C2 = {v} ; ::_thesis: verum
end;
assume A17: for C1 being Coset of W1
for C2 being Coset of W2 ex v being Element of M st C1 /\ C2 = {v} ; ::_thesis: M is_the_direct_sum_of W1,W2
A18: the carrier of W2 is Coset of W2 by VECTSP_4:73;
A19: the carrier of M c= the carrier of (W1 + W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of M or x in the carrier of (W1 + W2) )
assume x in the carrier of M ; ::_thesis: x in the carrier of (W1 + W2)
then reconsider u = x as Element of M ;
consider C1 being Coset of W1 such that
A20: u in C1 by VECTSP_4:68;
consider v being Element of M such that
A21: C1 /\ the carrier of W2 = {v} by A18, A17;
A22: v in {v} by TARSKI:def_1;
then v in C1 by A21, XBOOLE_0:def_4;
then consider v1 being Element of M such that
A23: v1 in W1 and
A24: u - v1 = v by A20, VECTSP_4:79;
v in the carrier of W2 by A21, A22, XBOOLE_0:def_4;
then A25: v in W2 by STRUCT_0:def_5;
u = v1 + v by A24, VECTSP_2:2;
then x in W1 + W2 by A25, A23, Th1;
hence x in the carrier of (W1 + W2) by STRUCT_0:def_5; ::_thesis: verum
end;
the carrier of W1 is Coset of W1 by VECTSP_4:73;
then consider v being Element of M such that
A26: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;
the carrier of (W1 + W2) c= the carrier of M by VECTSP_4:def_2;
then the carrier of M = the carrier of (W1 + W2) by A19, XBOOLE_0:def_10;
hence VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) = W1 + W2 by A1, VECTSP_4:31; :: according to VECTSP_5:def_4 ::_thesis: W1 /\ W2 = (0). M
0. M in W2 by VECTSP_4:17;
then A27: 0. M in the carrier of W2 by STRUCT_0:def_5;
0. M in W1 by VECTSP_4:17;
then 0. M in the carrier of W1 by STRUCT_0:def_5;
then A28: 0. M in {v} by A26, A27, XBOOLE_0:def_4;
the carrier of ((0). M) = {(0. M)} by VECTSP_4:def_3
.= the carrier of W1 /\ the carrier of W2 by A26, A28, TARSKI:def_1
.= the carrier of (W1 /\ W2) by Def2 ;
hence W1 /\ W2 = (0). M by VECTSP_4:29; ::_thesis: verum
end;
theorem :: VECTSP_5:47
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 )
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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 )
let W1, W2 be Subspace of M; ::_thesis: 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 )
let v, v1, v2, u1, u2 be Element of M; ::_thesis: ( 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 implies ( v1 = u1 & v2 = u2 ) )
reconsider C2 = v1 + W2 as Coset of W2 by VECTSP_4:def_6;
reconsider C1 = the carrier of W1 as Coset of W1 by VECTSP_4:73;
A1: v1 in C2 by VECTSP_4:44;
assume M is_the_direct_sum_of W1,W2 ; ::_thesis: ( not v = v1 + v2 or not v = u1 + u2 or not v1 in W1 or not u1 in W1 or not v2 in W2 or not u2 in W2 or ( v1 = u1 & v2 = u2 ) )
then consider u being Element of M such that
A2: C1 /\ C2 = {u} by Th46;
assume that
A3: ( v = v1 + v2 & v = u1 + u2 ) and
A4: v1 in W1 and
A5: u1 in W1 and
A6: ( v2 in W2 & u2 in W2 ) ; ::_thesis: ( v1 = u1 & v2 = u2 )
A7: v2 - u2 in W2 by A6, VECTSP_4:23;
v1 in C1 by A4, STRUCT_0:def_5;
then v1 in C1 /\ C2 by A1, XBOOLE_0:def_4;
then A8: v1 = u by A2, TARSKI:def_1;
A9: u1 in C1 by A5, STRUCT_0:def_5;
u1 = (v1 + v2) - u2 by A3, VECTSP_2:2
.= v1 + (v2 - u2) by RLVECT_1:def_3 ;
then u1 in C2 by A7;
then A10: u1 in C1 /\ C2 by A9, XBOOLE_0:def_4;
hence v1 = u1 by A2, A8, TARSKI:def_1; ::_thesis: v2 = u2
u1 = u by A10, A2, TARSKI:def_1;
hence v2 = u2 by A3, A8, RLVECT_1:8; ::_thesis: verum
end;
theorem :: VECTSP_5:49
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: ( 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 ) implies M is_the_direct_sum_of W1,W2 )
assume A1: M = W1 + W2 ; ::_thesis: ( for v being Element of M ex 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 & not ( v1 = u1 & v2 = u2 ) ) or M is_the_direct_sum_of W1,W2 )
( the carrier of ((0). M) = {(0. M)} & (0). M is Subspace of W1 /\ W2 ) by VECTSP_4:39, VECTSP_4:def_3;
then A2: {(0. M)} c= the carrier of (W1 /\ W2) by VECTSP_4:def_2;
given v being Element of M such that A3: 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 ) ; ::_thesis: M is_the_direct_sum_of W1,W2
assume not M is_the_direct_sum_of W1,W2 ; ::_thesis: contradiction
then W1 /\ W2 <> (0). M by A1, Def4;
then the carrier of (W1 /\ W2) <> {(0. M)} by VECTSP_4:def_3;
then {(0. M)} c< the carrier of (W1 /\ W2) by A2, XBOOLE_0:def_8;
then consider x being set such that
A4: x in the carrier of (W1 /\ W2) and
A5: not x in {(0. M)} by XBOOLE_0:6;
A6: x in W1 /\ W2 by A4, STRUCT_0:def_5;
then x in M by VECTSP_4:9;
then reconsider u = x as Element of M by STRUCT_0:def_5;
consider v1, v2 being Element of M such that
A7: v1 in W1 and
A8: v2 in W2 and
A9: v = v1 + v2 by A1, Lm16;
A10: v = (v1 + v2) + (0. M) by A9, RLVECT_1:4
.= (v1 + v2) + (u - u) by VECTSP_1:19
.= ((v1 + v2) + u) - u by RLVECT_1:def_3
.= ((v1 + u) + v2) - u by RLVECT_1:def_3
.= (v1 + u) + (v2 - u) by RLVECT_1:def_3 ;
x in W2 by A6, Th3;
then A11: v2 - u in W2 by A8, VECTSP_4:23;
x in W1 by A6, Th3;
then v1 + u in W1 by A7, VECTSP_4:20;
then v2 - u = v2 by A3, A7, A8, A9, A10, A11;
then v2 + (- u) = v2 + (0. M) by RLVECT_1:4;
then - u = 0. M by RLVECT_1:8;
then A12: u = - (0. M) by RLVECT_1:17;
x <> 0. M by A5, TARSKI:def_1;
hence contradiction by A12, RLVECT_1:12; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 ;
funcv |-- (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
ex b1 being Element of [: the carrier of M, the carrier of M:] st
( v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 )
proof
W1 + W2 = VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by A1, Def4;
then consider v1, v2 being Element of M such that
A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm16;
take [v1,v2] ; ::_thesis: ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 )
[v1,v2] `1 = v1 by MCART_1:7;
hence ( v = ([v1,v2] `1) + ([v1,v2] `2) & [v1,v2] `1 in W1 & [v1,v2] `2 in W2 ) by A2, MCART_1:7; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of [: the carrier of M, the carrier of M:] st v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 & v = (b2 `1) + (b2 `2) & b2 `1 in W1 & b2 `2 in W2 holds
b1 = b2
proof
let t1, t2 be Element of [: the carrier of M, the carrier of M:]; ::_thesis: ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 implies t1 = t2 )
assume ( v = (t1 `1) + (t1 `2) & t1 `1 in W1 & t1 `2 in W2 & v = (t2 `1) + (t2 `2) & t2 `1 in W1 & t2 `2 in W2 ) ; ::_thesis: t1 = t2
then A3: ( t1 `1 = t2 `1 & t1 `2 = t2 `2 ) by A1, Th48;
t1 = [(t1 `1),(t1 `2)] by MCART_1:21;
hence t1 = t2 by A3, MCART_1:21; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines |-- VECTSP_5:def_6_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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 b6 being Element of [: the carrier of M, the carrier of M:] holds
( b6 = v |-- (W1,W2) iff ( v = (b6 `1) + (b6 `2) & b6 `1 in W1 & b6 `2 in W2 ) );
theorem Th50: :: VECTSP_5:50
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let v be Element of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
then A2: (v |-- (W1,W2)) `2 in W2 by Def6;
A3: M is_the_direct_sum_of W2,W1 by A1, Lm17;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6;
( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6;
hence (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 by A1, A2, A4, A5, Th48; ::_thesis: verum
end;
theorem Th51: :: VECTSP_5:51
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: 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
let W1, W2 be Subspace of M; ::_thesis: for v being Element of M st M is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let v be Element of M; ::_thesis: ( M is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 )
assume A1: M is_the_direct_sum_of W1,W2 ; ::_thesis: (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
then A2: (v |-- (W1,W2)) `2 in W2 by Def6;
A3: M is_the_direct_sum_of W2,W1 by A1, Lm17;
then A4: ( v = ((v |-- (W2,W1)) `2) + ((v |-- (W2,W1)) `1) & (v |-- (W2,W1)) `1 in W2 ) by Def6;
A5: (v |-- (W2,W1)) `2 in W1 by A3, Def6;
( v = ((v |-- (W1,W2)) `1) + ((v |-- (W1,W2)) `2) & (v |-- (W1,W2)) `1 in W1 ) by A1, Def6;
hence (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 by A1, A2, A4, A5, Th48; ::_thesis: verum
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)
proof
let F be Field; ::_thesis: 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)
let V be VectSp of F; ::_thesis: 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)
let W be Subspace of V; ::_thesis: 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)
let L be Linear_Compl of W; ::_thesis: 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)
let v be Element of V; ::_thesis: 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)
let t be Element of [: the carrier of V, the carrier of V:]; ::_thesis: ( (t `1) + (t `2) = v & t `1 in W & t `2 in L implies t = v |-- (W,L) )
V is_the_direct_sum_of W,L by Th38;
hence ( (t `1) + (t `2) = v & t `1 in W & t `2 in L implies t = v |-- (W,L) ) by Def6; ::_thesis: verum
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
proof
let F be Field; ::_thesis: 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
let V be VectSp of F; ::_thesis: 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
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let v be Element of V; ::_thesis: ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
V is_the_direct_sum_of W,L by Th38;
hence ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v by Def6; ::_thesis: verum
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 )
proof
let F be Field; ::_thesis: 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 )
let V be VectSp of F; ::_thesis: 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 )
let W be Subspace of V; ::_thesis: 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 )
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
let v be Element of V; ::_thesis: ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
V is_the_direct_sum_of W,L by Th38;
hence ( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) by Def6; ::_thesis: verum
end;
theorem :: VECTSP_5:55
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 |-- (L,W)) `2
proof
let F be Field; ::_thesis: 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 |-- (L,W)) `2
let V be VectSp of F; ::_thesis: 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 |-- (L,W)) `2
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let v be Element of V; ::_thesis: (v |-- (W,L)) `1 = (v |-- (L,W)) `2
V is_the_direct_sum_of W,L by Th38;
hence (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th50; ::_thesis: verum
end;
theorem :: VECTSP_5:56
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)) `2 = (v |-- (L,W)) `1
proof
let F be Field; ::_thesis: 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)) `2 = (v |-- (L,W)) `1
let V be VectSp of F; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W
for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let L be Linear_Compl of W; ::_thesis: for v being Element of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let v be Element of V; ::_thesis: (v |-- (W,L)) `2 = (v |-- (L,W)) `1
V is_the_direct_sum_of W,L by Th38;
hence (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th51; ::_thesis: verum
end;
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
ex b1 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
b1 . (A1,A2) = W1 + W2
proof
defpred S1[ set , set , set ] means for W1, W2 being Subspace of M st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Subspaces M ex B being Element of Subspaces M st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces M; ::_thesis: ex B being Element of Subspaces M st S1[A1,A2,B]
consider W1 being strict Subspace of M such that
A2: W1 = A1 by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = A2 by Def3;
reconsider C = W1 + W2 as Element of Subspaces M by Def3;
take C ; ::_thesis: S1[A1,A2,C]
thus S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
thus ex o being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M holds S1[A1,A2,o . (A1,A2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces M); ::_thesis: ( ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (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
o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces M ex W1, W2 being Subspace of M st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 + W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_M_&_y_in_Subspaces_M_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces M & y in Subspaces M implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Subspaces M and
A7: y in Subspaces M ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Subspaces M by A6, A7;
consider W1 being strict Subspace of M such that
A8: W1 = x by A6, Def3;
consider W2 being strict Subspace of M such that
A9: W2 = y by A7, Def3;
o1 . (A,B) = W1 + W2 by A4, A8, A9;
hence o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines SubJoin VECTSP_5:def_7_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being BinOp of (Subspaces M) holds
( b3 = SubJoin M iff for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 + W2 );
definition
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ;
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr 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
ex b1 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
b1 . (A1,A2) = W1 /\ W2
proof
defpred S1[ set , set , set ] means for W1, W2 being Subspace of M st $1 = W1 & $2 = W2 holds
$3 = W1 /\ W2;
A1: for A1, A2 being Element of Subspaces M ex B being Element of Subspaces M st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces M; ::_thesis: ex B being Element of Subspaces M st S1[A1,A2,B]
consider W1 being strict Subspace of M such that
A2: W1 = A1 by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = A2 by Def3;
reconsider C = W1 /\ W2 as Element of Subspaces M by Def3;
take C ; ::_thesis: S1[A1,A2,C]
thus S1[A1,A2,C] by A2, A3; ::_thesis: verum
end;
thus ex o being BinOp of (Subspaces M) st
for A1, A2 being Element of Subspaces M holds S1[A1,A2,o . (A1,A2)] from BINOP_1:sch_3(A1); ::_thesis: verum
end;
uniqueness
for b1, b2 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
b1 . (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
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces M); ::_thesis: ( ( for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (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
o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 )
assume A4: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces M ex W1, W2 being Subspace of M st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 )
assume A5: for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ; ::_thesis: o1 = o2
now__::_thesis:_for_x,_y_being_set_st_x_in_Subspaces_M_&_y_in_Subspaces_M_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces M & y in Subspaces M implies o1 . (x,y) = o2 . (x,y) )
assume that
A6: x in Subspaces M and
A7: y in Subspaces M ; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider A = x, B = y as Element of Subspaces M by A6, A7;
consider W1 being strict Subspace of M such that
A8: W1 = x by A6, Def3;
consider W2 being strict Subspace of M such that
A9: W2 = y by A7, Def3;
o1 . (A,B) = W1 /\ W2 by A4, A8, A9;
hence o1 . (x,y) = o2 . (x,y) by A5, A8, A9; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines SubMeet VECTSP_5:def_8_:_
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
for b3 being BinOp of (Subspaces M) holds
( b3 = SubMeet M iff for A1, A2 being Element of Subspaces M
for W1, W2 being Subspace of M st A1 = W1 & A2 = W2 holds
b3 . (A1,A2) = W1 /\ W2 );
theorem Th57: :: VECTSP_5:57
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
A1: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" B = B "/\" A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" B = B "/\" A
consider W1 being strict Subspace of M such that
A2: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A3: W2 = B by Def3;
thus A "/\" B = (SubMeet M) . (A,B) by LATTICES:def_2
.= W1 /\ W2 by A2, A3, Def8
.= (SubMeet M) . (B,A) by A2, A3, Def8
.= B "/\" A by LATTICES:def_2 ; ::_thesis: verum
end;
A4: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds (A "/\" B) "\/" B = B
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: (A "/\" B) "\/" B = B
consider W1 being strict Subspace of M such that
A5: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A6: W2 = B by Def3;
reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus (A "/\" B) "\/" B = (SubJoin M) . ((A "/\" B),B) by LATTICES:def_1
.= (SubJoin M) . (((SubMeet M) . (A,B)),B) by LATTICES:def_2
.= (SubJoin M) . (AB,B) by A5, A6, Def8
.= (W1 /\ W2) + W2 by A6, Def7
.= B by A6, Lm10, VECTSP_4:29 ; ::_thesis: verum
end;
A7: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C
consider W1 being strict Subspace of M such that
A8: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A9: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A10: W3 = C by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (B "/\" C) = (SubMeet M) . (A,(B "/\" C)) by LATTICES:def_2
.= (SubMeet M) . (A,((SubMeet M) . (B,C))) by LATTICES:def_2
.= (SubMeet M) . (A,BC) by A9, A10, Def8
.= W1 /\ (W2 /\ W3) by A8, Def8
.= (W1 /\ W2) /\ W3 by Th14
.= (SubMeet M) . (AB,C) by A10, Def8
.= (SubMeet M) . (((SubMeet M) . (A,B)),C) by A8, A9, Def8
.= (SubMeet M) . ((A "/\" B),C) by LATTICES:def_2
.= (A "/\" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
A11: for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C
consider W1 being strict Subspace of M such that
A12: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A13: W2 = B by Def3;
consider W3 being strict Subspace of M such that
A14: W3 = C by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "\/" (B "\/" C) = (SubJoin M) . (A,(B "\/" C)) by LATTICES:def_1
.= (SubJoin M) . (A,((SubJoin M) . (B,C))) by LATTICES:def_1
.= (SubJoin M) . (A,BC) by A13, A14, Def7
.= W1 + (W2 + W3) by A12, Def7
.= (W1 + W2) + W3 by Th6
.= (SubJoin M) . (AB,C) by A14, Def7
.= (SubJoin M) . (((SubJoin M) . (A,B)),C) by A12, A13, Def7
.= (SubJoin M) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "\/" C by LATTICES:def_1 ; ::_thesis: verum
end;
A15: for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "/\" (A "\/" B) = A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "/\" (A "\/" B) = A
consider W1 being strict Subspace of M such that
A16: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A17: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "/\" (A "\/" B) = (SubMeet M) . (A,(A "\/" B)) by LATTICES:def_2
.= (SubMeet M) . (A,((SubJoin M) . (A,B))) by LATTICES:def_1
.= (SubMeet M) . (A,AB) by A16, A17, Def7
.= W1 /\ (W1 + W2) by A16, Def8
.= A by A16, Lm11, VECTSP_4:29 ; ::_thesis: verum
end;
for A, B being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds A "\/" B = B "\/" A
proof
let A, B be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: A "\/" B = B "\/" A
consider W1 being strict Subspace of M such that
A18: W1 = A by Def3;
consider W2 being strict Subspace of M such that
A19: W2 = B by Def3;
thus A "\/" B = (SubJoin M) . (A,B) by LATTICES:def_1
.= W1 + W2 by A18, A19, Def7
.= W2 + W1 by Lm1
.= (SubJoin M) . (B,A) by A18, A19, Def7
.= B "\/" A by LATTICES:def_1 ; ::_thesis: verum
end;
then ( LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-absorbing & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-commutative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is meet-associative & LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is join-absorbing ) by A11, A4, A1, A7, A15, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is Lattice ; ::_thesis: verum
end;
theorem Th58: :: VECTSP_5:58
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
proof
reconsider C = (0). M as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
take C ; ::_thesis: for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "/\" A = C & A "/\" C = C )
let A be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( C "/\" A = C & A "/\" C = C )
consider W being strict Subspace of M such that
A1: W = A by Def3;
thus C "/\" A = (SubMeet M) . (C,A) by LATTICES:def_2
.= ((0). M) /\ W by A1, Def8
.= C by Th20 ; ::_thesis: A "/\" C = C
thus A "/\" C = (SubMeet M) . (A,C) by LATTICES:def_2
.= W /\ ((0). M) by A1, Def8
.= C by Th20 ; ::_thesis: verum
end;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 0_Lattice by Th57, LATTICES:def_13; ::_thesis: verum
end;
theorem Th59: :: VECTSP_5:59
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
ex C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st
for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
proof
consider W9 being strict Subspace of M such that
A1: the carrier of W9 = the carrier of ((Omega). M) ;
reconsider C = W9 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
take C ; ::_thesis: for A being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) holds
( C "\/" A = C & A "\/" C = C )
let A be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( C "\/" A = C & A "\/" C = C )
consider W being strict Subspace of M such that
A2: W = A by Def3;
A3: C is Subspace of (Omega). M by Lm6;
thus C "\/" A = (SubJoin M) . (C,A) by LATTICES:def_1
.= W9 + W by A2, Def7
.= ((Omega). M) + W by A1, Lm5
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by Th11
.= C by A1, A3, VECTSP_4:31 ; ::_thesis: A "\/" C = C
thus A "\/" C = (SubJoin M) . (A,C) by LATTICES:def_1
.= W + W9 by A2, Def7
.= W + ((Omega). M) by A1, Lm5
.= VectSpStr(# the carrier of M, the addF of M, the ZeroF of M, the lmult of M #) by Th11
.= C by A1, A3, VECTSP_4:31 ; ::_thesis: verum
end;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 1_Lattice by Th57, LATTICES:def_14; ::_thesis: verum
end;
theorem Th60: :: VECTSP_5:60
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice
LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is lower-bounded upper-bounded Lattice by Th58, Th59;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is 01_Lattice ; ::_thesis: verum
end;
theorem :: VECTSP_5:61
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
proof
let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF; ::_thesis: LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice
set S = LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #);
for A, B, C being Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #); ::_thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
assume A1: A [= C ; ::_thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C
consider W1 being strict Subspace of M such that
A2: W1 = A by Def3;
consider W3 being strict Subspace of M such that
A3: W3 = C by Def3;
W1 + W3 = (SubJoin M) . (A,C) by A2, A3, Def7
.= A "\/" C by LATTICES:def_1
.= W3 by A1, A3, LATTICES:def_3 ;
then A4: W1 is Subspace of W3 by Th8;
consider W2 being strict Subspace of M such that
A5: W2 = B by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) by Def3;
thus A "\/" (B "/\" C) = (SubJoin M) . (A,(B "/\" C)) by LATTICES:def_1
.= (SubJoin M) . (A,((SubMeet M) . (B,C))) by LATTICES:def_2
.= (SubJoin M) . (A,BC) by A5, A3, Def8
.= W1 + (W2 /\ W3) by A2, Def7
.= (W1 + W2) /\ W3 by A4, Th30
.= (SubMeet M) . (AB,C) by A3, Def8
.= (SubMeet M) . (((SubJoin M) . (A,B)),C) by A2, A5, Def7
.= (SubMeet M) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
hence LattStr(# (Subspaces M),(SubJoin M),(SubMeet M) #) is M_Lattice by Th57, LATTICES:def_12; ::_thesis: verum
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
proof
let F be Field; ::_thesis: for V being VectSp of F holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
let V be VectSp of F; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th60;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
consider W9 being strict Subspace of V such that
A1: the carrier of W9 = the carrier of ((Omega). V) ;
reconsider I = W9 as Element of S by Def3;
reconsider I1 = I as Element of S1 ;
reconsider Z = (0). V as Element of S by Def3;
reconsider Z0 = Z as Element of S0 ;
now__::_thesis:_for_A_being_Element_of_S0_holds_A_"/\"_Z0_=_Z0
let A be Element of S0; ::_thesis: A "/\" Z0 = Z0
consider W being strict Subspace of V such that
A2: W = A by Def3;
thus A "/\" Z0 = (SubMeet V) . (A,Z0) by LATTICES:def_2
.= W /\ ((0). V) by A2, Def8
.= Z0 by Th20 ; ::_thesis: verum
end;
then A3: Bottom S = Z by RLSUB_2:64;
now__::_thesis:_for_A_being_Element_of_S1_holds_A_"\/"_I1_=_W9
let A be Element of S1; ::_thesis: A "\/" I1 = W9
consider W being strict Subspace of V such that
A4: W = A by Def3;
A5: W9 is Subspace of (Omega). V by Lm6;
thus A "\/" I1 = (SubJoin V) . (A,I1) by LATTICES:def_1
.= W + W9 by A4, Def7
.= W + ((Omega). V) by A1, Lm5
.= VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Th11
.= W9 by A1, A5, VECTSP_4:31 ; ::_thesis: verum
end;
then A6: Top S = I by RLSUB_2:65;
now__::_thesis:_for_A_being_Element_of_S_ex_B_being_Element_of_S_st_B_is_a_complement_of_A
A7: I is Subspace of (Omega). V by Lm6;
let A be Element of S; ::_thesis: ex B being Element of S st B is_a_complement_of A
consider W being strict Subspace of V such that
A8: W = A by Def3;
set L = the Linear_Compl of W;
consider W99 being strict Subspace of V such that
A9: the carrier of W99 = the carrier of the Linear_Compl of W by Lm4;
reconsider B9 = W99 as Element of S by Def3;
take B = B9; ::_thesis: B is_a_complement_of A
A10: B "/\" A = (SubMeet V) . (B,A) by LATTICES:def_2
.= W99 /\ W by A8, Def8
.= the Linear_Compl of W /\ W by A9, Lm8
.= Bottom S by A3, Th40 ;
B "\/" A = (SubJoin V) . (B,A) by LATTICES:def_1
.= W99 + W by A8, Def7
.= the Linear_Compl of W + W by A9, Lm5
.= VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) by Th39
.= Top S by A1, A6, A7, VECTSP_4:31 ;
hence B is_a_complement_of A by A10, LATTICES:def_18; ::_thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is C_Lattice by LATTICES:def_19; ::_thesis: verum
end;