environ
vocabularies HIDDEN, BHSP_1, RLSUB_1, ARYTM_3, STRUCT_0, RLVECT_1, SUBSET_1, TARSKI, SUPINF_2, XBOOLE_0, ARYTM_1, RLSUB_2, ZFMISC_1, FUNCT_1, RELAT_1, REAL_1, CARD_1, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1, PBOOLE;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, XCMPLX_0, XREAL_0, STRUCT_0, FUNCT_1, NUMBERS, BINOP_1, LATTICES, RELSET_1, REAL_1, DOMAIN_1, RLVECT_1, RLSUB_1, BHSP_1, RUSUB_1;
definitions TARSKI, XBOOLE_0;
theorems RLVECT_1, FUNCT_1, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, RLSUB_1, XBOOLE_1, RUSUB_1, RLSUB_2, MCART_1, BINOP_1, LATTICES, XCMPLX_0, ORDERS_1, STRUCT_0, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, RELSET_1, ORDERS_1, BINOP_1, CLASSES1;
registrations SUBSET_1, MEMBERED, STRUCT_0, LATTICES, BHSP_1, RUSUB_1, RELAT_1, XREAL_0, XTUPLE_0;
constructors HIDDEN, BINOP_1, REAL_1, MEMBERED, REALSET1, LATTICES, RLSUB_1, RUSUB_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities XBOOLE_0, RLVECT_1;
expansions TARSKI, XBOOLE_0;
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
Lm4:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of W1
Lm5:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ W2) c= the carrier of (W1 + W2)
Lm6:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of ((W1 /\ W2) + W2) = the carrier of W2
Lm7:
for V being RealUnitarySpace
for W1, W2 being Subspace of V holds the carrier of (W1 /\ (W1 + W2)) = the carrier of W1
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))
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))
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))
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))
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 #)
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 ) )
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
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
by Th14, Lm1;
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 ) )
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
definition
let V be
RealUnitarySpace;
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;
definition
let V be
RealUnitarySpace;
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;
registration
let V be
RealUnitarySpace;
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;
:: and coset of a subspace