:: RUSUB_2 semantic presentation
begin
definition
let V be RealUnitarySpace;
let W1, W2 be Subspace of V;
funcW1 + W2 -> strict Subspace of V means :Def1: :: RUSUB_2:def 1
the carrier of it = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
existence
ex b1 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
proof
reconsider V1 = the carrier of W1, V2 = the carrier of W2 as Subset of V by RUSUB_1:def_1;
set VS = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
{ (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } or x in the carrier of V )
assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: x in the carrier of V
then ex v1, v2 being VECTOR of V st
( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider VS = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } as Subset of V ;
A1: 0. V = (0. V) + (0. V) by RLVECT_1:4;
( 0. V in W1 & 0. V in W2 ) by RUSUB_1:11;
then A2: 0. V in VS by A1;
A3: VS = { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) }
proof
thus VS c= { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (v + u) where v, u is VECTOR of V : ( 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 VECTOR of V : ( v in V1 & u in V2 ) } )
assume x in VS ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) }
then consider v, u being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in V1 & u in V2 ) } or x in VS )
assume x in { (v + u) where v, u is VECTOR of V : ( v in V1 & u in V2 ) } ; ::_thesis: x in VS
then consider v, u being VECTOR of V 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 RUSUB_1:28;
hence ex b1 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A2, A3, RLSUB_1:6, RUSUB_1:29; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V st the carrier of b1 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } & the carrier of b2 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } holds
b1 = b2 by RUSUB_1:24;
end;
:: deftheorem Def1 defines + RUSUB_2:def_1_:_
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for b4 being strict Subspace of V holds
( b4 = W1 + W2 iff the carrier of b4 = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } );
definition
let V be RealUnitarySpace;
let W1, W2 be Subspace of V;
funcW1 /\ W2 -> strict Subspace of V means :Def2: :: RUSUB_2:def 2
the carrier of it = the carrier of W1 /\ the carrier of W2;
existence
ex b1 being strict Subspace of V 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 V;
0. V in W2 by RUSUB_1:11;
then A1: 0. V in the carrier of W2 by STRUCT_0:def_5;
( the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V ) by RUSUB_1:def_1;
then the carrier of W1 /\ the carrier of W2 c= the carrier of V /\ the carrier of V 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 V by RUSUB_1:def_1;
( V1 is linearly-closed & V2 is linearly-closed ) by RUSUB_1:28;
then A2: V3 is linearly-closed by RLSUB_1:7;
0. V in W1 by RUSUB_1:11;
then 0. V 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 V st the carrier of b1 = the carrier of W1 /\ the carrier of W2 by A2, RUSUB_1:29; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict Subspace of V 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 RUSUB_1:24;
end;
:: deftheorem Def2 defines /\ RUSUB_2:def_2_:_
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for b4 being strict Subspace of V holds
( b4 = W1 /\ W2 iff the carrier of b4 = the carrier of W1 /\ the carrier of W2 );
begin
theorem Th1: :: RUSUB_2:1
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for x being set holds
( x in W1 + W2 iff ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for x being set holds
( x in W1 + W2 iff ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let W1, W2 be Subspace of V; ::_thesis: for x being set holds
( x in W1 + W2 iff ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
let x be set ; ::_thesis: ( x in W1 + W2 iff ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) )
thus ( x in W1 + W2 implies ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & x = v1 + v2 ) ) ::_thesis: ( ex v1, v2 being VECTOR of V 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 VECTOR of V 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 VECTOR of V : ( v in W1 & u in W2 ) } by Def1;
then consider v1, v2 being VECTOR of V such that
A1: ( x = v1 + v2 & v1 in W1 & v2 in W2 ) ;
take v1 ; ::_thesis: ex v2 being VECTOR of V 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 VECTOR of V 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 VECTOR of V : ( 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: :: RUSUB_2:2
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let W1, W2 be Subspace of V; ::_thesis: for v being VECTOR of V st ( v in W1 or v in W2 ) holds
v in W1 + W2
let v be VECTOR of V; ::_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. V) & 0. V in W2 ) by RLVECT_1:4, RUSUB_1:11;
hence v in W1 + W2 by A2, Th1; ::_thesis: verum
end;
supposeA3: v in W2 ; ::_thesis: v in W1 + W2
( v = (0. V) + v & 0. V in W1 ) by RLVECT_1:4, RUSUB_1:11;
hence v in W1 + W2 by A3, Th1; ::_thesis: verum
end;
end;
end;
hence v in W1 + W2 ; ::_thesis: verum
end;
theorem Th3: :: RUSUB_2:3
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for x being set holds
( x in W1 /\ W2 iff ( x in W1 & x in W2 ) )
let W1, W2 be Subspace of V; ::_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;
Lm1: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1
let W1, W2 be Subspace of V; ::_thesis: W1 + W2 = W2 + W1
set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ;
A1: { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } c= { (v + u) where v, u is VECTOR of V : ( 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 VECTOR of V : ( v in W2 & u in W1 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } )
assume x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
then ex v, u being VECTOR of V st
( x = v + u & v in W2 & u in W1 ) ;
hence x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: verum
end;
A2: the carrier of (W1 + W2) = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by Def1;
{ (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } c= { (v + u) where v, u is VECTOR of V : ( 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 VECTOR of V : ( v in W1 & u in W2 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } )
assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) }
then ex v, u being VECTOR of V st
( x = v + u & v in W1 & u in W2 ) ;
hence x in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } ; ::_thesis: verum
end;
then { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W1 ) } by A1, XBOOLE_0:def_10;
hence W1 + W2 = W2 + W1 by A2, Def1; ::_thesis: verum
end;
Lm2: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
let W1, W2 be Subspace of V; ::_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 VECTOR of V : ( 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 VECTOR of V by RUSUB_1:3;
A1: v = v + (0. V) by RLVECT_1:4;
( v in W1 & 0. V in W2 ) by RUSUB_1:11, STRUCT_0:def_5;
then x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by A1;
hence x in the carrier of (W1 + W2) by Def1; ::_thesis: verum
end;
Lm3: for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
proof
let V be RealUnitarySpace; ::_thesis: for W1 being Subspace of V
for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W1 be Subspace of V; ::_thesis: for W2 being strict Subspace of V st the carrier of W1 c= the carrier of W2 holds
W1 + W2 = W2
let W2 be strict Subspace of V; ::_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 VECTOR of V : ( v in W1 & u in W2 ) } by Def1;
then consider v, u being VECTOR of V such that
A3: x = v + u and
A4: v in W1 and
A5: u in W2 ;
W1 is Subspace of W2 by A1, RUSUB_1:22;
then v in W2 by A4, RUSUB_1:1;
then v + u in W2 by A5, RUSUB_1:14;
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 RUSUB_1:24; ::_thesis: verum
end;
theorem :: RUSUB_2:4
for V being RealUnitarySpace
for W being strict Subspace of V holds W + W = W by Lm3;
theorem :: RUSUB_2:5
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1 by Lm1;
theorem Th6: :: RUSUB_2:6
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of V; ::_thesis: W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ;
A1: the carrier of (W1 + (W2 + W3)) = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } by Def1;
A2: { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where v, u is VECTOR of V : ( 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 VECTOR of V : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } )
assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
then consider v, u being VECTOR of V 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 VECTOR of V : ( v in W1 & u in W2 ) } by Def1;
then consider u1, u2 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 & u in W2 + W3 ) } by A3, A7, A9; ::_thesis: verum
end;
{ (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where v, u is VECTOR of V : ( 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 VECTOR of V : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } )
assume x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ; ::_thesis: x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
then consider v, u being VECTOR of V 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 VECTOR of V : ( v in W2 & u in W3 ) } by Def1;
then consider u1, u2 being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( v in W1 + W2 & u in W3 ) } by A10, A15, A16; ::_thesis: verum
end;
then { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } = { (v + u) where v, u is VECTOR of V : ( 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: :: RUSUB_2:7
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds
( W1 is Subspace of W1 + W2 & W2 is Subspace of W1 + W2 )
let W1, W2 be Subspace of V; ::_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 RUSUB_1:22; ::_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 RUSUB_1:22; ::_thesis: verum
end;
theorem Th8: :: RUSUB_2:8
for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
proof
let V be RealUnitarySpace; ::_thesis: for W1 being Subspace of V
for W2 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W1 be Subspace of V; ::_thesis: for W2 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 + W2 = W2 )
let W2 be strict Subspace of V; ::_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 RUSUB_1:def_1;
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: :: RUSUB_2:9
for V being RealUnitarySpace
for W being strict Subspace of V holds
( ((0). V) + W = W & W + ((0). V) = W )
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V holds
( ((0). V) + W = W & W + ((0). V) = W )
let W be strict Subspace of V; ::_thesis: ( ((0). V) + W = W & W + ((0). V) = W )
(0). V is Subspace of W by RUSUB_1:33;
then the carrier of ((0). V) c= the carrier of W by RUSUB_1:def_1;
hence ((0). V) + W = W by Lm3; ::_thesis: W + ((0). V) = W
hence W + ((0). V) = W by Lm1; ::_thesis: verum
end;
theorem Th10: :: RUSUB_2:10
for V being RealUnitarySpace holds
( ((0). V) + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
proof
let V be RealUnitarySpace; ::_thesis: ( ((0). V) + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
thus ((0). V) + ((Omega). V) = (Omega). V by Th9
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3 ; ::_thesis: ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
hence ((Omega). V) + ((0). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Lm1; ::_thesis: verum
end;
theorem Th11: :: RUSUB_2:11
for V being RealUnitarySpace
for W being Subspace of V holds
( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds
( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
let W be Subspace of V; ::_thesis: ( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
( the carrier of V = the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & the carrier of W c= the carrier of V ) by RUSUB_1:def_1;
then the carrier of W c= the carrier of ((Omega). V) by RUSUB_1:def_3;
then W + ((Omega). V) = (Omega). V by Lm3
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3 ;
hence ( ((Omega). V) + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & W + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) ) by Lm1; ::_thesis: verum
end;
theorem :: RUSUB_2:12
for V being strict RealUnitarySpace holds ((Omega). V) + ((Omega). V) = V by Th11;
theorem :: RUSUB_2:13
for V being RealUnitarySpace
for W being strict Subspace of V holds W /\ W = W
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V holds W /\ W = W
let W be strict Subspace of V; ::_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: :: RUSUB_2:14
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds W1 /\ W2 = W2 /\ W1
let W1, W2 be Subspace of V; ::_thesis: W1 /\ W2 = W2 /\ W1
the carrier of (W1 /\ W2) = the carrier of W2 /\ the carrier of W1 by Def2;
hence W1 /\ W2 = W2 /\ W1 by Def2; ::_thesis: verum
end;
theorem Th15: :: RUSUB_2:15
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V holds W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3
let W1, W2, W3 be Subspace of V; ::_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;
Lm4: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1
let W1, W2 be Subspace of V; ::_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 Th16: :: RUSUB_2:16
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let W1, W2 be Subspace of V; ::_thesis: ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
the carrier of (W1 /\ W2) c= the carrier of W1 by Lm4;
hence W1 /\ W2 is Subspace of W1 by RUSUB_1:22; ::_thesis: W1 /\ W2 is Subspace of W2
the carrier of (W2 /\ W1) c= the carrier of W2 by Lm4;
then the carrier of (W1 /\ W2) c= the carrier of W2 by Th14;
hence W1 /\ W2 is Subspace of W2 by RUSUB_1:22; ::_thesis: verum
end;
theorem Th17: :: RUSUB_2:17
for V being RealUnitarySpace
for W2 being Subspace of V
for W1 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 /\ W2 = W1 )
proof
let V be RealUnitarySpace; ::_thesis: for W2 being Subspace of V
for W1 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 /\ W2 = W1 )
let W2 be Subspace of V; ::_thesis: for W1 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 /\ W2 = W1 )
let W1 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 iff W1 /\ W2 = W1 )
thus ( W1 is Subspace of W2 implies W1 /\ W2 = W1 ) ::_thesis: ( W1 /\ W2 = W1 implies W1 is Subspace of W2 )
proof
assume W1 is Subspace of W2 ; ::_thesis: W1 /\ W2 = W1
then A1: the carrier of W1 c= the carrier of W2 by RUSUB_1:def_1;
the carrier of (W1 /\ W2) = the carrier of W1 /\ the carrier of W2 by Def2;
hence W1 /\ W2 = W1 by A1, RUSUB_1:24, XBOOLE_1:28; ::_thesis: verum
end;
thus ( W1 /\ W2 = W1 implies W1 is Subspace of W2 ) by Th16; ::_thesis: verum
end;
theorem Th18: :: RUSUB_2:18
for V being RealUnitarySpace
for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
let W be Subspace of V; ::_thesis: ( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )
0. V in W by RUSUB_1:11;
then 0. V in the carrier of W by STRUCT_0:def_5;
then {(0. V)} c= the carrier of W by ZFMISC_1:31;
then A1: {(0. V)} /\ the carrier of W = {(0. V)} by XBOOLE_1:28;
the carrier of (((0). V) /\ W) = the carrier of ((0). V) /\ the carrier of W by Def2
.= {(0. V)} /\ the carrier of W by RUSUB_1:def_2 ;
hence ((0). V) /\ W = (0). V by A1, RUSUB_1:def_2; ::_thesis: W /\ ((0). V) = (0). V
hence W /\ ((0). V) = (0). V by Th14; ::_thesis: verum
end;
theorem :: RUSUB_2:19
for V being RealUnitarySpace holds
( ((0). V) /\ ((Omega). V) = (0). V & ((Omega). V) /\ ((0). V) = (0). V ) by Th18;
theorem Th20: :: RUSUB_2:20
for V being RealUnitarySpace
for W being strict Subspace of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let W be strict Subspace of V; ::_thesis: ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
(Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3;
then A1: the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W by Def2;
the carrier of W c= the carrier of V by RUSUB_1:def_1;
hence ((Omega). V) /\ W = W by A1, RUSUB_1:24, XBOOLE_1:28; ::_thesis: W /\ ((Omega). V) = W
hence W /\ ((Omega). V) = W by Th14; ::_thesis: verum
end;
theorem :: RUSUB_2:21
for V being strict RealUnitarySpace holds ((Omega). V) /\ ((Omega). V) = V
proof
let V be strict RealUnitarySpace; ::_thesis: ((Omega). V) /\ ((Omega). V) = V
thus ((Omega). V) /\ ((Omega). V) = (Omega). V by Th20
.= V by RUSUB_1:def_3 ; ::_thesis: verum
end;
Lm5: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
let W1, W2 be Subspace of V; ::_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, Lm4;
hence the carrier of (W1 /\ W2) c= the carrier of (W1 + W2) by XBOOLE_1:1; ::_thesis: verum
end;
theorem :: RUSUB_2:22
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds W1 /\ W2 is Subspace of W1 + W2 by Lm5, RUSUB_1:22;
Lm6: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
let W1, W2 be Subspace of V; ::_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 VECTOR of V : ( u in W1 /\ W2 & v in W2 ) } by Def1;
then consider u, v being VECTOR of V 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, RUSUB_1:14;
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 :: RUSUB_2:23
for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds (W1 /\ W2) + W2 = W2 by Lm6, RUSUB_1:24;
Lm7: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
let W1, W2 be Subspace of V; ::_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 V by RUSUB_1:def_1;
then reconsider x1 = x as Element of V by A2;
A3: ( x1 + (0. V) = x1 & 0. V in W2 ) by RLVECT_1:4, RUSUB_1:11;
x in W1 by A2, STRUCT_0:def_5;
then x in { (u + v) where u, v is VECTOR of V : ( 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 :: RUSUB_2:24
for V being RealUnitarySpace
for W1 being Subspace of V
for W2 being strict Subspace of V holds W2 /\ (W2 + W1) = W2 by Lm7, RUSUB_1:24;
Lm8: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V holds the carrier of ((W1 /\ W2) + (W2 /\ W3)) c= the carrier of (W2 /\ (W1 + W3))
let W1, W2, W3 be Subspace of V; ::_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 VECTOR of V : ( u in W1 /\ W2 & v in W2 /\ W3 ) } by Def1;
then consider u, v being VECTOR of V 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, RUSUB_1:14;
( 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 :: RUSUB_2:25
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by Lm8, RUSUB_1:22;
Lm9: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
the carrier of (W2 /\ (W1 + W3)) = the carrier of ((W1 /\ W2) + (W2 /\ W3))
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V 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 V; ::_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 VECTOR of V : ( u in W1 & v in W3 ) } by Def1;
then consider u1, v1 being VECTOR of V such that
A3: x = u1 + v1 and
A4: u1 in W1 and
A5: v1 in W3 ;
A6: u1 in W2 by A1, A4, RUSUB_1:1;
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, RUSUB_1:17;
then v1 + (u1 - u1) in W2 by RLVECT_1:def_3;
then v1 + (0. V) in W2 by RLVECT_1:15;
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 Lm8; ::_thesis: verum
end;
theorem :: RUSUB_2:26
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3) by Lm9, RUSUB_1:24;
Lm10: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V holds the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3))
let W1, W2, W3 be Subspace of V; ::_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 VECTOR of V : ( u in W2 & v in W1 /\ W3 ) } by Def1;
then consider u, v being VECTOR of V 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 VECTOR of V : ( 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 VECTOR of V : ( 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 :: RUSUB_2:27
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V holds W2 + (W1 /\ W3) is Subspace of (W1 + W2) /\ (W2 + W3) by Lm10, RUSUB_1:22;
Lm11: for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
the carrier of (W2 + (W1 /\ W3)) = the carrier of ((W1 + W2) /\ (W2 + W3))
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V 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 V; ::_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 V by RUSUB_1:def_1;
A1: V2 is linearly-closed by RUSUB_1:28;
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 RUSUB_1:def_1;
thus the carrier of (W2 + (W1 /\ W3)) c= the carrier of ((W1 + W2) /\ (W2 + W3)) by Lm10; :: 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 VECTOR of V : ( u1 in W1 & u2 in W2 ) } by Def1;
then consider u1, u2 being VECTOR of V 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, RLSUB_1:def_1;
then A5: u1 + u2 in W2 by STRUCT_0:def_5;
( 0. V in W1 /\ W3 & (u1 + u2) + (0. V) = u1 + u2 ) by RLVECT_1:4, RUSUB_1:11;
then x in { (u + v) where u, v is VECTOR of V : ( 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 :: RUSUB_2:28
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3) by Lm11, RUSUB_1:24;
theorem Th29: :: RUSUB_2:29
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is strict Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being Subspace of V st W1 is strict Subspace of W3 holds
W1 + (W2 /\ W3) = (W1 + W2) /\ W3
let W1, W2, W3 be Subspace of V; ::_thesis: ( W1 is strict Subspace of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3 )
assume A1: W1 is strict Subspace of W3 ; ::_thesis: W1 + (W2 /\ W3) = (W1 + W2) /\ W3
thus (W1 + W2) /\ W3 = W3 /\ (W1 + W2) by Th14
.= (W1 /\ W3) + (W3 /\ W2) by A1, Lm9, RUSUB_1:24
.= W1 + (W3 /\ W2) by A1, Th17
.= W1 + (W2 /\ W3) by Th14 ; ::_thesis: verum
end;
theorem :: RUSUB_2:30
for V being RealUnitarySpace
for W1, W2 being strict Subspace of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being strict Subspace of V holds
( W1 + W2 = W2 iff W1 /\ W2 = W1 )
let W1, W2 be strict Subspace of V; ::_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 Th17; ::_thesis: verum
end;
theorem :: RUSUB_2:31
for V being RealUnitarySpace
for W1 being Subspace of V
for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
proof
let V be RealUnitarySpace; ::_thesis: for W1 being Subspace of V
for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let W1 be Subspace of V; ::_thesis: for W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 + W3 is Subspace of W2 + W3
let W2, W3 be strict Subspace of V; ::_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 :: RUSUB_2:32
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds
( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
let W1, W2 be Subspace of V; ::_thesis: ( ( W1 is Subspace of W2 or W2 is Subspace of W1 ) iff ex W being Subspace of V 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 V 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 V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
proof
given W being Subspace of V 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, RUSUB_1:22;
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 VECTOR of V by RUSUB_1:3;
reconsider A1 = the carrier of W as Subset of V by RUSUB_1:def_1;
A6: A1 is linearly-closed by RUSUB_1:28;
not the carrier of W1 c= the carrier of W2 by A2, RUSUB_1:22;
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 VECTOR of V by RUSUB_1:3;
A9: now__::_thesis:_not_x_+_y_in_the_carrier_of_W2
reconsider A2 = the carrier of W2 as Subset of V by RUSUB_1:def_1;
A10: A2 is linearly-closed by RUSUB_1:28;
assume x + y in the carrier of W2 ; ::_thesis: contradiction
then (x + y) - y in the carrier of W2 by A10, RLSUB_1:3;
then x + (y - y) in the carrier of W2 by RLVECT_1:def_3;
then x + (0. V) in the carrier of W2 by RLVECT_1:15;
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 V by RUSUB_1:def_1;
A12: A2 is linearly-closed by RUSUB_1:28;
assume x + y in the carrier of W1 ; ::_thesis: contradiction
then (y + x) - x in the carrier of W1 by A12, RLSUB_1:3;
then y + (x - x) in the carrier of W1 by RLVECT_1:def_3;
then y + (0. V) in the carrier of W1 by RLVECT_1:15;
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, RLSUB_1: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_V_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 V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W1 c= the carrier of W2 by RUSUB_1:def_1;
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 V 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_V_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 V st the carrier of W = the carrier of W1 \/ the carrier of W2 )
then the carrier of W2 c= the carrier of W1 by RUSUB_1:def_1;
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 V 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 V st the carrier of W = the carrier of W1 \/ the carrier of W2
hence ex W being Subspace of V st the carrier of W = the carrier of W1 \/ the carrier of W2 by A13, A14; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
func Subspaces V -> set means :Def3: :: RUSUB_2:def 3
for x being set holds
( x in it iff x is strict Subspace of V );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subspace of V )
proof
defpred S1[ set , set ] means ex W being strict Subspace of V st
( $2 = W & $1 = the carrier of W );
defpred S2[ set ] means ex W being strict Subspace of V 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 V & 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 RUSUB_1:24;
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 V 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 y is strict Subspace of V )
proof
let y be set ; ::_thesis: ( y in rng f iff y is strict Subspace of V )
thus ( y in rng f implies y is strict Subspace of V ) ::_thesis: ( y is strict Subspace of V implies y in rng f )
proof
assume y in rng f ; ::_thesis: y is strict Subspace of V
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 V st
( y = W & x = the carrier of W ) by A3;
hence y is strict Subspace of V ; ::_thesis: verum
end;
assume y is strict Subspace of V ; ::_thesis: y in rng f
then reconsider W = y as strict Subspace of V ;
reconsider x = the carrier of W as set ;
the carrier of W c= the carrier of V by RUSUB_1:def_1;
then A9: x in dom f by A1, A7;
then [x,y] in f by A3, A7;
then y = f . x by A9, FUNCT_1:def_2;
hence y in rng f by A9, FUNCT_1:def_3; ::_thesis: verum
end;
hence ex b1 being set st
for x being set holds
( x in b1 iff x is strict Subspace of V ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict Subspace of V ) ) & ( for x being set holds
( x in b2 iff x is strict Subspace of V ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff x is strict Subspace of V ) ) & ( for x being set holds
( x in D2 iff x is strict Subspace of V ) ) implies D1 = D2 )
assume A10: for x being set holds
( x in D1 iff x is strict Subspace of V ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies x is strict Subspace of V ) implies ( x is strict Subspace of V & not x in D2 ) ) or D1 = D2 )
assume A11: for x being set holds
( x in D2 iff x is strict Subspace of V ) ; ::_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 x is strict Subspace of V by A10;
hence x in D2 by A11; ::_thesis: verum
end;
assume x in D2 ; ::_thesis: x in D1
then x is strict Subspace of V by A11;
hence x in D1 by A10; ::_thesis: verum
end;
hence D1 = D2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Subspaces RUSUB_2:def_3_:_
for V being RealUnitarySpace
for b2 being set holds
( b2 = Subspaces V iff for x being set holds
( x in b2 iff x is strict Subspace of V ) );
registration
let V be RealUnitarySpace;
cluster Subspaces V -> non empty ;
coherence
not Subspaces V is empty
proof
set x = the strict Subspace of V;
the strict Subspace of V in Subspaces V by Def3;
hence not Subspaces V is empty ; ::_thesis: verum
end;
end;
theorem :: RUSUB_2:33
for V being strict RealUnitarySpace holds V in Subspaces V
proof
let V be strict RealUnitarySpace; ::_thesis: V in Subspaces V
(Omega). V in Subspaces V by Def3;
hence V in Subspaces V by RUSUB_1:def_3; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
let W1, W2 be Subspace of V;
predV is_the_direct_sum_of W1,W2 means :Def4: :: RUSUB_2:def 4
( UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2 & W1 /\ W2 = (0). V );
end;
:: deftheorem Def4 defines is_the_direct_sum_of RUSUB_2:def_4_:_
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( V is_the_direct_sum_of W1,W2 iff ( UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2 & W1 /\ W2 = (0). V ) );
Lm12: for V being RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
proof
let V be RealUnitarySpace; ::_thesis: for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
let W be strict Subspace of V; ::_thesis: ( ( for v being VECTOR of V holds v in W ) implies W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
assume A1: for v being VECTOR of V holds v in W ; ::_thesis: W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
now__::_thesis:_for_v_being_VECTOR_of_V_holds_
(_(_v_in_W_implies_v_in_(Omega)._V_)_&_(_v_in_(Omega)._V_implies_v_in_W_)_)
let v be VECTOR of V; ::_thesis: ( ( v in W implies v in (Omega). V ) & ( v in (Omega). V implies v in W ) )
thus ( v in W implies v in (Omega). V ) ::_thesis: ( v in (Omega). V implies v in W )
proof
assume v in W ; ::_thesis: v in (Omega). V
v in UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RLVECT_1:1;
hence v in (Omega). V by RUSUB_1:def_3; ::_thesis: verum
end;
assume v in (Omega). V ; ::_thesis: v in W
thus v in W by A1; ::_thesis: verum
end;
then W = (Omega). V by RUSUB_1:25;
hence W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RUSUB_1:def_3; ::_thesis: verum
end;
Lm13: for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds
( W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
let W1, W2 be Subspace of V; ::_thesis: ( W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
thus ( W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) implies for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) ::_thesis: ( ( for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) implies W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
proof
assume A1: W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) ; ::_thesis: for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
let v be VECTOR of V; ::_thesis: ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 )
v in UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RLVECT_1:1;
hence ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) by A1, Th1; ::_thesis: verum
end;
assume A2: for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ; ::_thesis: W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
now__::_thesis:_for_u_being_VECTOR_of_V_holds_u_in_W1_+_W2
let u be VECTOR of V; ::_thesis: u in W1 + W2
ex v1, v2 being VECTOR of V 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 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Lm12; ::_thesis: verum
end;
Lm14: for V being RealUnitarySpace
for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V ex C being strict Subspace of V st V is_the_direct_sum_of C,W
let W be Subspace of V; ::_thesis: ex C being strict Subspace of V st V is_the_direct_sum_of C,W
defpred S1[ 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 & S1[x] ) ) from XBOOLE_0:sch_1();
( W /\ ((0). V) = (0). V & (0). V in Subspaces V ) by Def3, Th18;
then reconsider X = X as non empty set by A1;
defpred S2[ set , set ] means ex W1, W2 being strict Subspace of V st
( $1 = W1 & $2 = W2 & W1 is Subspace of W2 );
consider R being Relation of X such that
A2: for x, y being Element of X holds
( [x,y] in R iff S2[x,y] ) from RELSET_1:sch_2();
defpred S3[ set , set ] means [$1,$2] in R;
A3: 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
A4: S3[x,y] and
A5: S3[y,z] ; ::_thesis: S3[x,z]
consider W1, W2 being strict Subspace of V such that
A6: x = W1 and
A7: ( y = W2 & W1 is Subspace of W2 ) by A2, A4;
consider W3, W4 being strict Subspace of V such that
A8: y = W3 and
A9: z = W4 and
A10: W3 is Subspace of W4 by A2, A5;
W1 is strict Subspace of W4 by A7, A8, A10, RUSUB_1:21;
hence S3[x,z] by A2, A6, A9; ::_thesis: verum
end;
A11: 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
A12: Y c= X and
A13: 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 <> {} ) ;
supposeA14: 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 A14; ::_thesis: verum
end;
supposeA15: 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 );
A16: 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
A17: x = W1 and
W /\ W1 = (0). V by A1, A12;
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 A17; ::_thesis: verum
end;
consider f being Function such that
A18: dom f = Y and
A19: for x being set st x in Y holds
S4[x,f . x] from CLASSES1:sch_1(A16);
set Z = union (rng f);
A20: 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
A21: x in Y9 and
A22: Y9 in rng f by TARSKI:def_4;
consider y being set such that
A23: y in dom f and
A24: f . y = Y9 by A22, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
y = W1 and
A25: f . y = the carrier of W1 by A18, A19, A23;
the carrier of W1 c= the carrier of V by RUSUB_1:def_1;
hence x in the carrier of V by A21, A24, A25; ::_thesis: verum
end;
set z = the Element of rng f;
A26: rng f <> {} by A15, A18, RELAT_1:42;
then consider z1 being set such that
A27: z1 in dom f and
A28: f . z1 = the Element of rng f by FUNCT_1:def_3;
reconsider Z = union (rng f) as Subset of V by A20, TARSKI:def_3;
ex W3 being strict Subspace of V st
( z1 = W3 & f . z1 = the carrier of W3 ) by A18, A19, A27;
then A29: Z <> {} by A26, A28, ORDERS_1:6;
A30: for v1, v2 being VECTOR of V st v1 in Z & v2 in Z holds
v1 + v2 in Z
proof
let v1, v2 be VECTOR of V; ::_thesis: ( v1 in Z & v2 in Z implies v1 + v2 in Z )
assume that
A31: v1 in Z and
A32: v2 in Z ; ::_thesis: v1 + v2 in Z
consider Y1 being set such that
A33: v1 in Y1 and
A34: Y1 in rng f by A31, TARSKI:def_4;
consider y1 being set such that
A35: y1 in dom f and
A36: f . y1 = Y1 by A34, FUNCT_1:def_3;
consider Y2 being set such that
A37: v2 in Y2 and
A38: Y2 in rng f by A32, TARSKI:def_4;
consider y2 being set such that
A39: y2 in dom f and
A40: f . y2 = Y2 by A38, FUNCT_1:def_3;
consider W1 being strict Subspace of V such that
A41: y1 = W1 and
A42: f . y1 = the carrier of W1 by A18, A19, A35;
consider W2 being strict Subspace of V such that
A43: y2 = W2 and
A44: f . y2 = the carrier of W2 by A18, A19, A39;
reconsider y1 = y1, y2 = y2 as Element of X by A12, A18, A35, A39;
now__::_thesis:_v1_+_v2_in_Z
percases ( [y1,y2] in R or [y2,y1] in R ) by A13, A18, A35, A39;
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 A41, A43, RUSUB_1:def_1;
then A45: v1 in W2 by A33, A36, A42, STRUCT_0:def_5;
v2 in W2 by A37, A40, A44, STRUCT_0:def_5;
then v1 + v2 in W2 by A45, RUSUB_1:14;
then A46: v1 + v2 in the carrier of W2 by STRUCT_0:def_5;
f . y2 in rng f by A39, FUNCT_1:def_3;
hence v1 + v2 in Z by A44, A46, 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 A41, A43, RUSUB_1:def_1;
then A47: v2 in W1 by A37, A40, A44, STRUCT_0:def_5;
v1 in W1 by A33, A36, A42, STRUCT_0:def_5;
then v1 + v2 in W1 by A47, RUSUB_1:14;
then A48: v1 + v2 in the carrier of W1 by STRUCT_0:def_5;
f . y1 in rng f by A35, FUNCT_1:def_3;
hence v1 + v2 in Z by A42, A48, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
hence v1 + v2 in Z ; ::_thesis: verum
end;
for a being Real
for v1 being VECTOR of V st v1 in Z holds
a * v1 in Z
proof
let a be Real; ::_thesis: for v1 being VECTOR of V st v1 in Z holds
a * v1 in Z
let v1 be VECTOR of V; ::_thesis: ( v1 in Z implies a * v1 in Z )
assume v1 in Z ; ::_thesis: a * v1 in Z
then consider Y1 being set such that
A49: v1 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;
consider W1 being strict Subspace of V such that
y1 = W1 and
A53: f . y1 = the carrier of W1 by A18, A19, A51;
v1 in W1 by A49, A52, A53, STRUCT_0:def_5;
then a * v1 in W1 by RUSUB_1:15;
then A54: a * v1 in the carrier of W1 by STRUCT_0:def_5;
f . y1 in rng f by A51, FUNCT_1:def_3;
hence a * v1 in Z by A53, A54, TARSKI:def_4; ::_thesis: verum
end;
then Z is linearly-closed by A30, RLSUB_1:def_1;
then consider E being strict Subspace of V such that
A55: Z = the carrier of E by A29, RUSUB_1:29;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_
(_(_u_in_W_/\_E_implies_u_in_(0)._V_)_&_(_u_in_(0)._V_implies_u_in_W_/\_E_)_)
let u be VECTOR 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 A56: u in W /\ E ; ::_thesis: u in (0). V
then A57: u in W by Th3;
u in E by A56, Th3;
then u in Z by A55, STRUCT_0:def_5;
then consider Y1 being set such that
A58: u in Y1 and
A59: Y1 in rng f by TARSKI:def_4;
consider y1 being set such that
A60: y1 in dom f and
A61: f . y1 = Y1 by A59, FUNCT_1:def_3;
A62: ex W2 being strict Subspace of V st
( y1 = W2 & W /\ W2 = (0). V ) by A1, A12, A18, A60;
consider W1 being strict Subspace of V such that
A63: y1 = W1 and
A64: f . y1 = the carrier of W1 by A18, A19, A60;
u in W1 by A58, A61, A64, STRUCT_0:def_5;
hence u in (0). V by A63, A57, A62, 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 RUSUB_1:def_2;
then u = 0. V by TARSKI:def_1;
hence u in W /\ E by RUSUB_1:11; ::_thesis: verum
end;
then A65: W /\ E = (0). V by RUSUB_1:25;
E in Subspaces V by Def3;
then reconsider y9 = E as Element of X by A1, A65;
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 A66: x in Y ; ::_thesis: [x,y] in R
then consider W1 being strict Subspace of V such that
A67: x = W1 and
A68: f . x = the carrier of W1 by A19;
now__::_thesis:_for_u_being_VECTOR_of_V_st_u_in_W1_holds_
u_in_E
let u be VECTOR of V; ::_thesis: ( u in W1 implies u in E )
assume u in W1 ; ::_thesis: u in E
then A69: u in the carrier of W1 by STRUCT_0:def_5;
the carrier of W1 in rng f by A18, A66, A68, FUNCT_1:def_3;
then u in Z by A69, TARSKI:def_4;
hence u in E by A55, STRUCT_0:def_5; ::_thesis: verum
end;
then W1 is strict Subspace of E by RUSUB_1:23;
hence [x,y] in R by A2, A67; ::_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;
A70: now__::_thesis:_for_x_being_Element_of_X_holds_x_is_strict_Subspace_of_V
let x be Element of X; ::_thesis: x is strict Subspace of V
x in Subspaces V by A1;
hence x is strict Subspace of V by Def3; ::_thesis: verum
end;
A71: now__::_thesis:_for_x_being_Element_of_X_holds_S3[x,x]
let x be Element of X; ::_thesis: S3[x,x]
reconsider W = x as strict Subspace of V by A70;
W is Subspace of W by RUSUB_1:19;
hence S3[x,x] by A2; ::_thesis: verum
end;
A72: 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 RUSUB_1:20; ::_thesis: verum
end;
consider x being Element of X such that
A73: for y being Element of X st x <> y holds
not S3[x,y] from ORDERS_1:sch_1(A71, A72, A3, A11);
consider L being strict Subspace of V such that
A74: x = L and
A75: W /\ L = (0). V by A1;
take L ; ::_thesis: V is_the_direct_sum_of L,W
thus UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = L + W :: according to RUSUB_2:def_4 ::_thesis: L /\ W = (0). V
proof
assume not UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = L + W ; ::_thesis: contradiction
then consider v being VECTOR of V such that
A76: for v1, v2 being VECTOR of V holds
( not v1 in L or not v2 in W or v <> v1 + v2 ) by Lm13;
( v = (0. V) + v & 0. V in W ) by RLVECT_1:4, RUSUB_1:11;
then A77: not v in L by A76;
set A = { (a * v) where a is Real : verum } ;
A78: 1 * v in { (a * v) where a is Real : verum } ;
now__::_thesis:_for_x_being_set_st_x_in__{__(a_*_v)_where_a_is_Real_:_verum__}__holds_
x_in_the_carrier_of_V
let x be set ; ::_thesis: ( x in { (a * v) where a is Real : verum } implies x in the carrier of V )
assume x in { (a * v) where a is Real : verum } ; ::_thesis: x in the carrier of V
then ex a being Real st x = a * v ;
hence x in the carrier of V ; ::_thesis: verum
end;
then reconsider A = { (a * v) where a is Real : verum } as Subset of V by TARSKI:def_3;
A79: for v1, v2 being VECTOR of V st v1 in A & v2 in A holds
v1 + v2 in A
proof
let v1, v2 be VECTOR 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 Real such that
A80: v1 = a1 * v ;
assume v2 in A ; ::_thesis: v1 + v2 in A
then consider a2 being Real such that
A81: v2 = a2 * v ;
v1 + v2 = (a1 + a2) * v by A80, A81, RLVECT_1:def_6;
hence v1 + v2 in A ; ::_thesis: verum
end;
for a being Real
for v1 being VECTOR of V st v1 in A holds
a * v1 in A
proof
let a be Real; ::_thesis: for v1 being VECTOR of V st v1 in A holds
a * v1 in A
let v1 be VECTOR of V; ::_thesis: ( v1 in A implies a * v1 in A )
assume v1 in A ; ::_thesis: a * v1 in A
then consider a1 being Real such that
A82: v1 = a1 * v ;
a * v1 = (a * a1) * v by A82, RLVECT_1:def_7;
hence a * v1 in A ; ::_thesis: verum
end;
then A is linearly-closed by A79, RLSUB_1:def_1;
then consider Z being strict Subspace of V such that
A83: the carrier of Z = A by A78, RUSUB_1:29;
A84: not v in L + W by A76, Th1;
now__::_thesis:_for_u_being_VECTOR_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 VECTOR 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 A85: u in Z /\ (W + L) ; ::_thesis: u in (0). V
then u in Z by Th3;
then u in A by A83, STRUCT_0:def_5;
then consider a being Real such that
A86: u = a * v ;
now__::_thesis:_not_a_<>_0
u in W + L by A85, Th3;
then (a ") * (a * v) in W + L by A86, RUSUB_1:15;
then A87: ((a ") * a) * v in W + L by RLVECT_1:def_7;
assume a <> 0 ; ::_thesis: contradiction
then 1 * v in W + L by A87, XCMPLX_0:def_7;
then 1 * v in L + W by Lm1;
hence contradiction by A84, RLVECT_1:def_8; ::_thesis: verum
end;
then u = 0. V by A86, RLVECT_1:10;
hence u in (0). V by RUSUB_1:11; ::_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 RUSUB_1:def_2;
then u = 0. V by TARSKI:def_1;
hence u in Z /\ (W + L) by RUSUB_1:11; ::_thesis: verum
end;
then A88: Z /\ (W + L) = (0). V by RUSUB_1:25;
now__::_thesis:_for_u_being_VECTOR_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 VECTOR 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 A89: u in (Z + L) /\ W ; ::_thesis: u in (0). V
then u in Z + L by Th3;
then consider v1, v2 being VECTOR of V such that
A90: v1 in Z and
A91: v2 in L and
A92: u = v1 + v2 by Th1;
A93: u in W by A89, Th3;
then A94: u in W + L by Th2;
( v1 = u - v2 & v2 in W + L ) by A91, A92, Th2, RLSUB_2:61;
then v1 in W + L by A94, RUSUB_1:17;
then v1 in Z /\ (W + L) by A90, Th3;
then v1 in the carrier of ((0). V) by A88, STRUCT_0:def_5;
then v1 in {(0. V)} by RUSUB_1:def_2;
then v1 = 0. V by TARSKI:def_1;
then v2 = u by A92, RLVECT_1:4;
hence u in (0). V by A75, A91, A93, 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 RUSUB_1:def_2;
then u = 0. V by TARSKI:def_1;
hence u in (Z + L) /\ W by RUSUB_1:11; ::_thesis: verum
end;
then (Z + L) /\ W = (0). V by RUSUB_1:25;
then A95: W /\ (Z + L) = (0). V by Th14;
Z + L in Subspaces V by Def3;
then reconsider x1 = Z + L as Element of X by A1, A95;
L is Subspace of Z + L by Th7;
then A96: [x,x1] in R by A2, A74;
v in A by A78, RLVECT_1:def_8;
then v in Z by A83, STRUCT_0:def_5;
then Z + L <> L by A77, Th2;
hence contradiction by A73, A74, A96; ::_thesis: verum
end;
thus L /\ W = (0). V by A75, Th14; ::_thesis: verum
end;
definition
let V be RealUnitarySpace;
let W be Subspace of V;
mode Linear_Compl of W -> Subspace of V means :Def5: :: RUSUB_2: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
ex C being strict Subspace of V st V is_the_direct_sum_of C,W by Lm14;
hence ex b1 being Subspace of V st V is_the_direct_sum_of b1,W ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Linear_Compl RUSUB_2:def_5_:_
for V being RealUnitarySpace
for W, b3 being Subspace of V holds
( b3 is Linear_Compl of W iff V is_the_direct_sum_of b3,W );
registration
let V be RealUnitarySpace;
let W be Subspace of V;
cluster non empty V99() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for Linear_Compl of W;
existence
ex b1 being Linear_Compl of W st b1 is strict
proof
consider C being strict Subspace of V such that
A1: V is_the_direct_sum_of C,W by Lm14;
C is Linear_Compl of W by A1, Def5;
hence ex b1 being Linear_Compl of W st b1 is strict ; ::_thesis: verum
end;
end;
Lm15: for V being RealUnitarySpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1 )
assume A1: V is_the_direct_sum_of W1,W2 ; ::_thesis: V is_the_direct_sum_of W2,W1
then W1 /\ W2 = (0). V by Def4;
then A2: W2 /\ W1 = (0). V by Th14;
UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2 by A1, Def4;
then UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W2 + W1 by Lm1;
hence V is_the_direct_sum_of W2,W1 by A2, Def4; ::_thesis: verum
end;
theorem :: RUSUB_2:34
for V being RealUnitarySpace
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 V be RealUnitarySpace; ::_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 Lm15;
hence W2 is Linear_Compl of W1 by Def5; ::_thesis: verum
end;
theorem Th35: :: RUSUB_2:35
for V being RealUnitarySpace
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 V be RealUnitarySpace; ::_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 Lm15; ::_thesis: verum
end;
begin
theorem Th36: :: RUSUB_2:36
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W holds
( W + L = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
let W be Subspace of V; ::_thesis: for L being Linear_Compl of W holds
( W + L = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
let L be Linear_Compl of W; ::_thesis: ( W + L = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) )
V is_the_direct_sum_of W,L by Th35;
hence W + L = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Def4; ::_thesis: L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #)
hence L + W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Lm1; ::_thesis: verum
end;
theorem Th37: :: RUSUB_2:37
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W holds
( W /\ L = (0). V & L /\ W = (0). V )
proof
let V be RealUnitarySpace; ::_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 )
V is_the_direct_sum_of W,L by Th35;
hence W /\ L = (0). V by Def4; ::_thesis: L /\ W = (0). V
hence L /\ W = (0). V by Th14; ::_thesis: verum
end;
theorem :: RUSUB_2:38
for V being RealUnitarySpace
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is_the_direct_sum_of W2,W1 by Lm15;
theorem Th39: :: RUSUB_2:39
for V being RealUnitarySpace holds
( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
proof
let V be RealUnitarySpace; ::_thesis: ( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V )
( ((0). V) + ((Omega). V) = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) & (0). V = ((0). V) /\ ((Omega). V) ) by Th10, Th18;
hence V is_the_direct_sum_of (0). V, (Omega). V by Def4; ::_thesis: V is_the_direct_sum_of (Omega). V, (0). V
hence V is_the_direct_sum_of (Omega). V, (0). V by Lm15; ::_thesis: verum
end;
theorem :: RUSUB_2:40
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L
proof
let V be RealUnitarySpace; ::_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 Lm15;
hence W is Linear_Compl of L by Def5; ::_thesis: verum
end;
theorem :: RUSUB_2:41
for V being RealUnitarySpace holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V )
proof
let V be RealUnitarySpace; ::_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 Th39;
hence ( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Def5; ::_thesis: verum
end;
Lm16: for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let W be Subspace of V; ::_thesis: for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let v be VECTOR of V; ::_thesis: for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
let x be set ; ::_thesis: ( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) )
thus ( x in v + W implies ex u being VECTOR of V st
( u in W & x = v + u ) ) ::_thesis: ( ex u being VECTOR of V st
( u in W & x = v + u ) implies x in v + W )
proof
assume x in v + W ; ::_thesis: ex u being VECTOR of V st
( u in W & x = v + u )
then x in { (v + u) where u is VECTOR of V : u in W } by RUSUB_1:def_4;
then consider u being VECTOR of V such that
A1: ( x = v + u & u in W ) ;
take u ; ::_thesis: ( u in W & x = v + u )
thus ( u in W & x = v + u ) by A1; ::_thesis: verum
end;
given u being VECTOR of V such that A2: ( u in W & x = v + u ) ; ::_thesis: x in v + W
x in { (v + v1) where v1 is VECTOR of V : v1 in W } by A2;
hence x in v + W by RUSUB_1:def_4; ::_thesis: verum
end;
theorem Th42: :: RUSUB_2:42
for V being RealUnitarySpace
for W1, W2 being Subspace of V
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 V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
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 V; ::_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 V by TARSKI:def_3;
v in C1 by A1, XBOOLE_0:def_4;
then A2: C1 = v + W1 by RUSUB_1:72;
v in C2 by A1, XBOOLE_0:def_4;
then A3: C2 = v + W2 by RUSUB_1:72;
reconsider v = v as VECTOR of V ;
A4: v + (W1 /\ W2) c= C1 /\ C2
proof
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 VECTOR of V such that
A5: u in W1 /\ W2 and
A6: x = v + u by Lm16;
u in W2 by A5, Th3;
then x in { (v + u2) where u2 is VECTOR of V : u2 in W2 } by A6;
then A7: x in C2 by A3, RUSUB_1:def_4;
u in W1 by A5, Th3;
then x in { (v + u1) where u1 is VECTOR of V : u1 in W1 } by A6;
then x in C1 by A2, RUSUB_1:def_4;
hence x in C1 /\ C2 by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
C1 /\ C2 c= v + (W1 /\ W2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C1 /\ C2 or x in v + (W1 /\ W2) )
assume A8: x in C1 /\ C2 ; ::_thesis: x in v + (W1 /\ W2)
then x in C1 by XBOOLE_0:def_4;
then consider u1 being VECTOR of V such that
A9: u1 in W1 and
A10: x = v + u1 by A2, Lm16;
x in C2 by A8, XBOOLE_0:def_4;
then consider u2 being VECTOR of V such that
A11: u2 in W2 and
A12: x = v + u2 by A3, Lm16;
u1 = u2 by A10, A12, RLVECT_1:8;
then u1 in W1 /\ W2 by A9, A11, Th3;
then x in { (v + u) where u is VECTOR of V : u in W1 /\ W2 } by A10;
hence x in v + (W1 /\ W2) by RUSUB_1:def_4; ::_thesis: verum
end;
then C1 /\ C2 = v + (W1 /\ W2) by A4, XBOOLE_0:def_10;
hence C1 /\ C2 is Coset of W1 /\ W2 by RUSUB_1:def_5; ::_thesis: verum
end;
Lm17: for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C
let W be Subspace of V; ::_thesis: for v being VECTOR of V ex C being Coset of W st v in C
let v be VECTOR of V; ::_thesis: ex C being Coset of W st v in C
reconsider C = v + W as Coset of W by RUSUB_1:def_5;
take C ; ::_thesis: v in C
thus v in C by RUSUB_1:37; ::_thesis: verum
end;
theorem Th43: :: RUSUB_2:43
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} )
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V holds
( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} )
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} )
set VW1 = the carrier of W1;
set VW2 = the carrier of W2;
0. V in W2 by RUSUB_1:11;
then A1: 0. V in the carrier of W2 by STRUCT_0:def_5;
thus ( V is_the_direct_sum_of W1,W2 implies for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) ::_thesis: ( ( for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v} ) implies V is_the_direct_sum_of W1,W2 )
proof
assume A2: V is_the_direct_sum_of W1,W2 ; ::_thesis: for C1 being Coset of W1
for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v}
then A3: UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2 by Def4;
let C1 be Coset of W1; ::_thesis: for C2 being Coset of W2 ex v being VECTOR of V st C1 /\ C2 = {v}
let C2 be Coset of W2; ::_thesis: ex v being VECTOR of V st C1 /\ C2 = {v}
consider v1 being VECTOR of V such that
A4: C1 = v1 + W1 by RUSUB_1:def_5;
v1 in UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RLVECT_1:1;
then consider v11, v12 being VECTOR of V such that
A5: v11 in W1 and
A6: v12 in W2 and
A7: v1 = v11 + v12 by A3, Th1;
consider v2 being VECTOR of V such that
A8: C2 = v2 + W2 by RUSUB_1:def_5;
v2 in UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RLVECT_1:1;
then consider v21, v22 being VECTOR of V 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, RLSUB_2:61;
then v21 in C2 by A8, A10, RUSUB_1:58;
then C2 = v21 + W2 by RUSUB_1:72;
then A14: x in C2 by A6, A13, RUSUB_1:57;
v12 = v1 - v11 by A7, RLSUB_2:61;
then v12 in C1 by A4, A5, RUSUB_1:58;
then C1 = v12 + W1 by RUSUB_1:72;
then x in C1 by A9, A13, RUSUB_1:57;
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 Th42;
A16: v in {v} by TARSKI:def_1;
W1 /\ W2 = (0). V by A2, Def4;
then ex u being VECTOR of V st C = {u} by RUSUB_1:67;
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 VECTOR of V st C1 /\ C2 = {v} ; ::_thesis: V is_the_direct_sum_of W1,W2
A18: the carrier of W2 is Coset of W2 by RUSUB_1:68;
now__::_thesis:_for_u_being_VECTOR_of_V_holds_u_in_W1_+_W2
let u be VECTOR of V; ::_thesis: u in W1 + W2
consider C1 being Coset of W1 such that
A19: u in C1 by Lm17;
consider v being VECTOR of V such that
A20: C1 /\ the carrier of W2 = {v} by A18, A17;
A21: v in {v} by TARSKI:def_1;
then v in C1 by A20, XBOOLE_0:def_4;
then consider v1 being VECTOR of V such that
A22: v1 in W1 and
A23: u - v1 = v by A19, RUSUB_1:74;
v in the carrier of W2 by A20, A21, XBOOLE_0:def_4;
then A24: v in W2 by STRUCT_0:def_5;
u = v1 + v by A23, RLSUB_2:61;
hence u in W1 + W2 by A24, A22, Th1; ::_thesis: verum
end;
hence UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) = W1 + W2 by Lm12; :: according to RUSUB_2:def_4 ::_thesis: W1 /\ W2 = (0). V
the carrier of W1 is Coset of W1 by RUSUB_1:68;
then consider v being VECTOR of V such that
A25: the carrier of W1 /\ the carrier of W2 = {v} by A18, A17;
0. V in W1 by RUSUB_1:11;
then 0. V in the carrier of W1 by STRUCT_0:def_5;
then A26: 0. V in {v} by A25, A1, XBOOLE_0:def_4;
the carrier of ((0). V) = {(0. V)} by RUSUB_1:def_2
.= the carrier of W1 /\ the carrier of W2 by A25, A26, TARSKI:def_1
.= the carrier of (W1 /\ W2) by Def2 ;
hence W1 /\ W2 = (0). V by RUSUB_1:24; ::_thesis: verum
end;
begin
theorem :: RUSUB_2:44
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) iff for v being VECTOR of V ex v1, v2 being VECTOR of V st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) ) by Lm13;
theorem Th45: :: RUSUB_2:45
for V being RealUnitarySpace
for W1, W2 being Subspace of V
for v, v1, v2, u1, u2 being VECTOR of V st V 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 V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V
for v, v1, v2, u1, u2 being VECTOR of V st V 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 V; ::_thesis: for v, v1, v2, u1, u2 being VECTOR of V st V 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 VECTOR of V; ::_thesis: ( V 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 RUSUB_1:def_5;
reconsider C1 = the carrier of W1 as Coset of W1 by RUSUB_1:68;
A1: v1 in C2 by RUSUB_1:37;
assume V 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 VECTOR of V such that
A2: C1 /\ C2 = {u} by Th43;
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, RUSUB_1:17;
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, RLSUB_2:61
.= v1 + (v2 - u2) by RLVECT_1:def_3 ;
then u1 in C2 by A7, Lm16;
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 :: RUSUB_2:46
for V being RealUnitarySpace
for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st
for v1, v2, u1, u2 being VECTOR of V 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
V is_the_direct_sum_of W1,W2
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2 being Subspace of V st V = W1 + W2 & ex v being VECTOR of V st
for v1, v2, u1, u2 being VECTOR of V 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
V is_the_direct_sum_of W1,W2
let W1, W2 be Subspace of V; ::_thesis: ( V = W1 + W2 & ex v being VECTOR of V st
for v1, v2, u1, u2 being VECTOR of V 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 V is_the_direct_sum_of W1,W2 )
assume A1: V = W1 + W2 ; ::_thesis: ( for v being VECTOR of V ex v1, v2, u1, u2 being VECTOR of V 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 V is_the_direct_sum_of W1,W2 )
( the carrier of ((0). V) = {(0. V)} & (0). V is Subspace of W1 /\ W2 ) by RUSUB_1:33, RUSUB_1:def_2;
then A2: {(0. V)} c= the carrier of (W1 /\ W2) by RUSUB_1:def_1;
given v being VECTOR of V such that A3: for v1, v2, u1, u2 being VECTOR of V 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: V is_the_direct_sum_of W1,W2
assume not V is_the_direct_sum_of W1,W2 ; ::_thesis: contradiction
then W1 /\ W2 <> (0). V by A1, Def4;
then the carrier of (W1 /\ W2) <> {(0. V)} by RUSUB_1:def_2;
then {(0. V)} 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. V)} by XBOOLE_0:6;
A6: x <> 0. V by A5, TARSKI:def_1;
A7: x in W1 /\ W2 by A4, STRUCT_0:def_5;
then x in V by RUSUB_1:2;
then reconsider u = x as VECTOR of V by STRUCT_0:def_5;
consider v1, v2 being VECTOR of V such that
A8: v1 in W1 and
A9: v2 in W2 and
A10: v = v1 + v2 by A1, Lm13;
A11: v = (v1 + v2) + (0. V) by A10, RLVECT_1:4
.= (v1 + v2) + (u - u) by RLVECT_1:15
.= ((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 A7, Th3;
then A12: v2 - u in W2 by A9, RUSUB_1:17;
x in W1 by A7, Th3;
then v1 + u in W1 by A8, RUSUB_1:14;
then v2 - u = v2 by A3, A8, A9, A10, A11, A12
.= v2 - (0. V) by RLVECT_1:13 ;
hence contradiction by A6, RLVECT_1:23; ::_thesis: verum
end;
definition
let V be RealUnitarySpace;
let v be VECTOR of V;
let W1, W2 be Subspace of V;
assume A1: V is_the_direct_sum_of W1,W2 ;
funcv |-- (W1,W2) -> Element of [: the carrier of V, the carrier of V:] means :Def6: :: RUSUB_2:def 6
( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );
existence
ex b1 being Element of [: the carrier of V, the carrier of V:] st
( v = (b1 `1) + (b1 `2) & b1 `1 in W1 & b1 `2 in W2 )
proof
W1 + W2 = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by A1, Def4;
then consider v1, v2 being VECTOR of V such that
A2: ( v1 in W1 & v2 in W2 & v = v1 + v2 ) by Lm13;
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 V, the carrier of V:] 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 V, the carrier of V:]; ::_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, Th45;
t1 = [(t1 `1),(t1 `2)] by MCART_1:21;
hence t1 = t2 by A3, MCART_1:21; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines |-- RUSUB_2:def_6_:_
for V being RealUnitarySpace
for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
for b5 being Element of [: the carrier of V, the carrier of V:] holds
( b5 = v |-- (W1,W2) iff ( v = (b5 `1) + (b5 `2) & b5 `1 in W1 & b5 `2 in W2 ) );
theorem Th47: :: RUSUB_2:47
for V being RealUnitarySpace
for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let v be VECTOR of V; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `1 = (v |-- (W2,W1)) `2 )
assume A1: V 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: V is_the_direct_sum_of W2,W1 by A1, Lm15;
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, Th45; ::_thesis: verum
end;
theorem Th48: :: RUSUB_2:48
for V being RealUnitarySpace
for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
proof
let V be RealUnitarySpace; ::_thesis: for v being VECTOR of V
for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let v be VECTOR of V; ::_thesis: for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds
(v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1
let W1, W2 be Subspace of V; ::_thesis: ( V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2)) `2 = (v |-- (W2,W1)) `1 )
assume A1: V 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: V is_the_direct_sum_of W2,W1 by A1, Lm15;
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, Th45; ::_thesis: verum
end;
theorem :: RUSUB_2:49
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 VECTOR 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 VECTOR 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)
V is_the_direct_sum_of W,L by Th35;
hence for v being VECTOR 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) by Def6; ::_thesis: verum
end;
theorem :: RUSUB_2:50
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v
V is_the_direct_sum_of W,L by Th35;
hence for v being VECTOR of V holds ((v |-- (W,L)) `1) + ((v |-- (W,L)) `2) = v by Def6; ::_thesis: verum
end;
theorem :: RUSUB_2:51
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 VECTOR 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 VECTOR of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L )
V is_the_direct_sum_of W,L by Th35;
hence for v being VECTOR of V holds
( (v |-- (W,L)) `1 in W & (v |-- (W,L)) `2 in L ) by Def6; ::_thesis: verum
end;
theorem :: RUSUB_2:52
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2
V is_the_direct_sum_of W,L by Th35;
hence for v being VECTOR of V holds (v |-- (W,L)) `1 = (v |-- (L,W)) `2 by Th47; ::_thesis: verum
end;
theorem :: RUSUB_2:53
for V being RealUnitarySpace
for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
proof
let V be RealUnitarySpace; ::_thesis: for W being Subspace of V
for L being Linear_Compl of W
for v being VECTOR 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 VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
let L be Linear_Compl of W; ::_thesis: for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1
V is_the_direct_sum_of W,L by Th35;
hence for v being VECTOR of V holds (v |-- (W,L)) `2 = (v |-- (L,W)) `1 by Th48; ::_thesis: verum
end;
begin
definition
let V be RealUnitarySpace;
func SubJoin V -> BinOp of (Subspaces V) means :Def7: :: RUSUB_2:def 7
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 + W2;
existence
ex b1 being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2
proof
defpred S1[ Element of Subspaces V, Element of Subspaces V, Element of Subspaces V] means for W1, W2 being Subspace of V st $1 = W1 & $2 = W2 holds
$3 = W1 + W2;
A1: for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces V; ::_thesis: ex B being Element of Subspaces V st S1[A1,A2,B]
reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;
reconsider C = W1 + W2 as Element of Subspaces V by Def3;
take C ; ::_thesis: S1[A1,A2,C]
thus S1[A1,A2,C] ; ::_thesis: verum
end;
ex o being BinOp of (Subspaces V) st
for a, b being Element of Subspaces V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
hence ex b1 being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces V); ::_thesis: ( ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 + W2 ) implies o1 = o2 )
assume A2: for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 + W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 + W2 ) or o1 = o2 )
assume A3: for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V 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_V_&_y_in_Subspaces_V_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces V & y in Subspaces V implies o1 . (x,y) = o2 . (x,y) )
assume A4: ( x in Subspaces V & y in Subspaces V ) ; ::_thesis: o1 . (x,y) = o2 . (x,y)
then reconsider A = x, B = y as Element of Subspaces V ;
reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;
o1 . (A,B) = W1 + W2 by A2;
hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines SubJoin RUSUB_2:def_7_:_
for V being RealUnitarySpace
for b2 being BinOp of (Subspaces V) holds
( b2 = SubJoin V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 + W2 );
definition
let V be RealUnitarySpace;
func SubMeet V -> BinOp of (Subspaces V) means :Def8: :: RUSUB_2:def 8
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
it . (A1,A2) = W1 /\ W2;
existence
ex b1 being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2
proof
defpred S1[ Element of Subspaces V, Element of Subspaces V, Element of Subspaces V] means for W1, W2 being Subspace of V st $1 = W1 & $2 = W2 holds
$3 = W1 /\ W2;
A1: for A1, A2 being Element of Subspaces V ex B being Element of Subspaces V st S1[A1,A2,B]
proof
let A1, A2 be Element of Subspaces V; ::_thesis: ex B being Element of Subspaces V st S1[A1,A2,B]
reconsider W1 = A1, W2 = A2 as Subspace of V by Def3;
reconsider C = W1 /\ W2 as Element of Subspaces V by Def3;
take C ; ::_thesis: S1[A1,A2,C]
thus S1[A1,A2,C] ; ::_thesis: verum
end;
ex o being BinOp of (Subspaces V) st
for a, b being Element of Subspaces V holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
hence ex b1 being BinOp of (Subspaces V) st
for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being BinOp of (Subspaces V) st ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (Subspaces V); ::_thesis: ( ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ) & ( for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o2 . (A1,A2) = W1 /\ W2 ) implies o1 = o2 )
assume A2: for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
o1 . (A1,A2) = W1 /\ W2 ; ::_thesis: ( ex A1, A2 being Element of Subspaces V ex W1, W2 being Subspace of V st
( A1 = W1 & A2 = W2 & not o2 . (A1,A2) = W1 /\ W2 ) or o1 = o2 )
assume A3: for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V 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_V_&_y_in_Subspaces_V_holds_
o1_._(x,y)_=_o2_._(x,y)
let x, y be set ; ::_thesis: ( x in Subspaces V & y in Subspaces V implies o1 . (x,y) = o2 . (x,y) )
assume A4: ( x in Subspaces V & y in Subspaces V ) ; ::_thesis: o1 . (x,y) = o2 . (x,y)
then reconsider A = x, B = y as Element of Subspaces V ;
reconsider W1 = x, W2 = y as Subspace of V by A4, Def3;
o1 . (A,B) = W1 /\ W2 by A2;
hence o1 . (x,y) = o2 . (x,y) by A3; ::_thesis: verum
end;
hence o1 = o2 by BINOP_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines SubMeet RUSUB_2:def_8_:_
for V being RealUnitarySpace
for b2 being BinOp of (Subspaces V) holds
( b2 = SubMeet V iff for A1, A2 being Element of Subspaces V
for W1, W2 being Subspace of V st A1 = W1 & A2 = W2 holds
b2 . (A1,A2) = W1 /\ W2 );
begin
theorem Th54: :: RUSUB_2:54
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
A1: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" B = B "/\" A
proof
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" B = B "/\" A
reconsider W1 = A, W2 = B as Subspace of V by Def3;
thus A "/\" B = (SubMeet V) . (A,B) by LATTICES:def_2
.= W1 /\ W2 by Def8
.= W2 /\ W1 by Th14
.= (SubMeet V) . (B,A) by Def8
.= B "/\" A by LATTICES:def_2 ; ::_thesis: verum
end;
A2: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds (A "/\" B) "\/" B = B
proof
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: (A "/\" B) "\/" B = B
reconsider W1 = A, W2 = B as strict Subspace of V by Def3;
reconsider AB = W1 /\ W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
thus (A "/\" B) "\/" B = (SubJoin V) . ((A "/\" B),B) by LATTICES:def_1
.= (SubJoin V) . (((SubMeet V) . (A,B)),B) by LATTICES:def_2
.= (SubJoin V) . (AB,B) by Def8
.= (W1 /\ W2) + W2 by Def7
.= B by Lm6, RUSUB_1:24 ; ::_thesis: verum
end;
A3: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" (B "\/" C) = (A "\/" B) "\/" C
proof
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" (B "\/" C) = (A "\/" B) "\/" C
reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;
reconsider AB = W1 + W2, BC = W2 + W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "\/" (B "\/" C) = (SubJoin V) . (A,(B "\/" C)) by LATTICES:def_1
.= (SubJoin V) . (A,((SubJoin V) . (B,C))) by LATTICES:def_1
.= (SubJoin V) . (A,BC) by Def7
.= W1 + (W2 + W3) by Def7
.= (W1 + W2) + W3 by Th6
.= (SubJoin V) . (AB,C) by Def7
.= (SubJoin V) . (((SubJoin V) . (A,B)),C) by Def7
.= (SubJoin V) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "\/" C by LATTICES:def_1 ; ::_thesis: verum
end;
A4: for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (A "\/" B) = A
proof
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (A "\/" B) = A
reconsider W1 = A, W2 = B as strict Subspace of V by Def3;
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "/\" (A "\/" B) = (SubMeet V) . (A,(A "\/" B)) by LATTICES:def_2
.= (SubMeet V) . (A,((SubJoin V) . (A,B))) by LATTICES:def_1
.= (SubMeet V) . (A,AB) by Def7
.= W1 /\ (W1 + W2) by Def8
.= A by Lm7, RUSUB_1:24 ; ::_thesis: verum
end;
A5: for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "/\" (B "/\" C) = (A "/\" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "/\" (B "/\" C) = (A "/\" B) "/\" C
reconsider W1 = A, W2 = B, W3 = C as Subspace of V by Def3;
reconsider AB = W1 /\ W2, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
thus A "/\" (B "/\" C) = (SubMeet V) . (A,(B "/\" C)) by LATTICES:def_2
.= (SubMeet V) . (A,((SubMeet V) . (B,C))) by LATTICES:def_2
.= (SubMeet V) . (A,BC) by Def8
.= W1 /\ (W2 /\ W3) by Def8
.= (W1 /\ W2) /\ W3 by Th15
.= (SubMeet V) . (AB,C) by Def8
.= (SubMeet V) . (((SubMeet V) . (A,B)),C) by Def8
.= (SubMeet V) . ((A "/\" B),C) by LATTICES:def_2
.= (A "/\" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
for A, B being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds A "\/" B = B "\/" A
proof
let A, B be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: A "\/" B = B "\/" A
reconsider W1 = A, W2 = B as Subspace of V by Def3;
thus A "\/" B = (SubJoin V) . (A,B) by LATTICES:def_1
.= W1 + W2 by Def7
.= W2 + W1 by Lm1
.= (SubJoin V) . (B,A) by Def7
.= B "\/" A by LATTICES:def_1 ; ::_thesis: verum
end;
then ( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-absorbing & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-commutative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is meet-associative & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is join-absorbing ) by A3, A2, A1, A5, A4, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice ; ::_thesis: verum
end;
registration
let V be RealUnitarySpace;
cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> Lattice-like ;
coherence
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th54;
end;
theorem Th55: :: RUSUB_2:55
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
ex C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )
proof
reconsider C = (0). V as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
take C ; ::_thesis: for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "/\" A = C & A "/\" C = C )
let A be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "/\" A = C & A "/\" C = C )
reconsider W = A as Subspace of V by Def3;
thus C "/\" A = (SubMeet V) . (C,A) by LATTICES:def_2
.= ((0). V) /\ W by Def8
.= C by Th18 ; ::_thesis: A "/\" C = C
hence A "/\" C = C ; ::_thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded by LATTICES:def_13; ::_thesis: verum
end;
theorem Th56: :: RUSUB_2:56
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
ex C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st
for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
proof
reconsider C = (Omega). V as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
take C ; ::_thesis: for A being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) holds
( C "\/" A = C & A "\/" C = C )
let A be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( C "\/" A = C & A "\/" C = C )
reconsider W = A as Subspace of V by Def3;
thus C "\/" A = (SubJoin V) . (C,A) by LATTICES:def_1
.= ((Omega). V) + W by Def7
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Th11
.= C by RUSUB_1:def_3 ; ::_thesis: A "\/" C = C
hence A "\/" C = C ; ::_thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded by LATTICES:def_14; ::_thesis: verum
end;
theorem Th57: :: RUSUB_2:57
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice
LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded upper-bounded Lattice by Th55, Th56;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is 01_Lattice ; ::_thesis: verum
end;
theorem Th58: :: RUSUB_2:58
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
for A, B, C being Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) st A [= C holds
A "\/" (B "/\" C) = (A "\/" B) "/\" C
proof
let A, B, C be Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #); ::_thesis: ( A [= C implies A "\/" (B "/\" C) = (A "\/" B) "/\" C )
reconsider W1 = A, W2 = B, W3 = C as strict Subspace of V by Def3;
assume A1: A [= C ; ::_thesis: A "\/" (B "/\" C) = (A "\/" B) "/\" C
reconsider AB = W1 + W2 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
reconsider BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
W1 + W3 = (SubJoin V) . (A,C) by Def7
.= A "\/" C by LATTICES:def_1
.= W3 by A1, LATTICES:def_3 ;
then A2: W1 is Subspace of W3 by Th8;
thus A "\/" (B "/\" C) = (SubJoin V) . (A,(B "/\" C)) by LATTICES:def_1
.= (SubJoin V) . (A,((SubMeet V) . (B,C))) by LATTICES:def_2
.= (SubJoin V) . (A,BC) by Def8
.= W1 + (W2 /\ W3) by Def7
.= (W1 + W2) /\ W3 by A2, Th29
.= (SubMeet V) . (AB,C) by Def8
.= (SubMeet V) . (((SubJoin V) . (A,B)),C) by Def7
.= (SubMeet V) . ((A "\/" B),C) by LATTICES:def_1
.= (A "\/" B) "/\" C by LATTICES:def_2 ; ::_thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular by LATTICES:def_12; ::_thesis: verum
end;
theorem Th59: :: RUSUB_2:59
for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented
proof
let V be RealUnitarySpace; ::_thesis: LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented
reconsider S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) as 01_Lattice by Th57;
reconsider S0 = S as 0_Lattice ;
reconsider S1 = S as 1_Lattice ;
reconsider Z = (0). V, I = (Omega). V as Element of S by Def3;
reconsider Z0 = Z as Element of S0 ;
reconsider I1 = I as Element of S1 ;
now__::_thesis:_for_A_being_Element_of_S0_holds_A_"/\"_Z0_=_Z0
let A be Element of S0; ::_thesis: A "/\" Z0 = Z0
reconsider W = A as Subspace of V by Def3;
thus A "/\" Z0 = (SubMeet V) . (A,Z0) by LATTICES:def_2
.= W /\ ((0). V) by Def8
.= Z0 by Th18 ; ::_thesis: verum
end;
then A1: Bottom S = Z by RLSUB_2:64;
now__::_thesis:_for_A_being_Element_of_S1_holds_A_"\/"_I1_=_(Omega)._V
let A be Element of S1; ::_thesis: A "\/" I1 = (Omega). V
reconsider W = A as Subspace of V by Def3;
thus A "\/" I1 = (SubJoin V) . (A,I1) by LATTICES:def_1
.= W + ((Omega). V) by Def7
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Th11
.= (Omega). V by RUSUB_1:def_3 ; ::_thesis: verum
end;
then A2: 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
let A be Element of S; ::_thesis: ex B being Element of S st B is_a_complement_of A
reconsider W = A as Subspace of V by Def3;
set L = the strict Linear_Compl of W;
reconsider B9 = the strict Linear_Compl of W as Element of S by Def3;
take B = B9; ::_thesis: B is_a_complement_of A
A3: B "/\" A = (SubMeet V) . (B,A) by LATTICES:def_2
.= the strict Linear_Compl of W /\ W by Def8
.= Bottom S by A1, Th37 ;
B "\/" A = (SubJoin V) . (B,A) by LATTICES:def_1
.= the strict Linear_Compl of W + W by Def7
.= UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Th36
.= Top S by A2, RUSUB_1:def_3 ;
hence B is_a_complement_of A by A3, LATTICES:def_18; ::_thesis: verum
end;
hence LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented by LATTICES:def_19; ::_thesis: verum
end;
registration
let V be RealUnitarySpace;
cluster LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) -> modular lower-bounded upper-bounded complemented ;
coherence
( LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is modular & LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented ) by Th55, Th56, Th58, Th59;
end;
theorem :: RUSUB_2:60
for V being RealUnitarySpace
for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
proof
let V be RealUnitarySpace; ::_thesis: for W1, W2, W3 being strict Subspace of V st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let W1, W2, W3 be strict Subspace of V; ::_thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )
set S = LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #);
reconsider A = W1, B = W2, C = W3, AC = W1 /\ W3, BC = W2 /\ W3 as Element of LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) by Def3;
assume A1: W1 is Subspace of W2 ; ::_thesis: W1 /\ W3 is Subspace of W2 /\ W3
A "\/" B = (SubJoin V) . (A,B) by LATTICES:def_1
.= W1 + W2 by Def7
.= B by A1, Th8 ;
then A [= B by LATTICES:def_3;
then A "/\" C [= B "/\" C by LATTICES:9;
then A2: (A "/\" C) "\/" (B "/\" C) = B "/\" C by LATTICES:def_3;
A3: B "/\" C = (SubMeet V) . (B,C) by LATTICES:def_2
.= W2 /\ W3 by Def8 ;
(A "/\" C) "\/" (B "/\" C) = (SubJoin V) . ((A "/\" C),(B "/\" C)) by LATTICES:def_1
.= (SubJoin V) . (((SubMeet V) . (A,C)),(B "/\" C)) by LATTICES:def_2
.= (SubJoin V) . (((SubMeet V) . (A,C)),((SubMeet V) . (B,C))) by LATTICES:def_2
.= (SubJoin V) . (((SubMeet V) . (A,C)),BC) by Def8
.= (SubJoin V) . (AC,BC) by Def8
.= (W1 /\ W3) + (W2 /\ W3) by Def7 ;
hence W1 /\ W3 is Subspace of W2 /\ W3 by A2, A3, Th8; ::_thesis: verum
end;
begin
theorem :: RUSUB_2:61
for V being RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of V holds v in W ) holds
W = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by Lm12;
theorem :: RUSUB_2:62
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V ex C being Coset of W st v in C by Lm17;
theorem :: RUSUB_2:63
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V
for x being set holds
( x in v + W iff ex u being VECTOR of V st
( u in W & x = v + u ) ) by Lm16;