begin
:: deftheorem Def1 defines + RUSUB_2:def 1 :
:: deftheorem Def2 defines /\ RUSUB_2:def 2 :
begin
theorem Th1:
theorem Th2:
theorem Th3:
Lm1:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds W1 + W2 = W2 + W1
Lm2:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
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
theorem
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
Lm4:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem
Lm5:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
theorem
Lm6:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
theorem
Lm7:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
theorem
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))
theorem
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))
theorem
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))
theorem
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))
theorem
theorem Th29:
theorem
theorem
theorem
begin
:: deftheorem Def3 defines Subspaces RUSUB_2:def 3 :
theorem
begin
:: deftheorem Def4 defines is_the_direct_sum_of RUSUB_2:def 4 :
Lm12:
for V being RealUnitarySpace
for W being strict Subspace of V st ( for v being VECTOR of holds v in W ) holds
W = UNITSTR(# the carrier of V,the U2 of V,the U7 of V,the Mult of V,the scalar of V #)
Lm13:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds
( W1 + W2 = UNITSTR(# the carrier of V,the U2 of V,the U7 of V,the Mult of V,the scalar of V #) iff for v being VECTOR of ex v1, v2 being VECTOR of st
( v1 in W1 & v2 in W2 & v = v1 + v2 ) )
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
:: deftheorem Def5 defines Linear_Compl RUSUB_2:def 5 :
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
theorem
theorem Th35:
begin
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem
theorem
Lm16:
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of
for x being set holds
( x in v + W iff ex u being VECTOR of st
( u in W & x = v + u ) )
theorem Th42:
Lm17:
for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of ex C being Coset of W st v in C
theorem Th43:
begin
theorem
theorem Th45:
theorem
:: deftheorem Def6 defines |-- RUSUB_2:def 6 :
theorem Th47:
theorem Th48:
theorem
theorem
theorem
theorem
theorem
begin
definition
let V be
RealUnitarySpace;
func SubJoin V -> BinOp of
Subspaces V means :
Def7:
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
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
end;
:: deftheorem Def7 defines SubJoin RUSUB_2:def 7 :
definition
let V be
RealUnitarySpace;
func SubMeet V -> BinOp of
Subspaces V means :
Def8:
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
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
end;
:: deftheorem Def8 defines SubMeet RUSUB_2:def 8 :
begin
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
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
begin
theorem
theorem
theorem