:: by Noboru Endou , Takashi Mitsuishi and Yasunari Shidama

::

:: Received October 9, 2002

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

definition

let V be RealUnitarySpace;

let W1, W2 be Subspace of V;

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

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

b_{1} = b_{2}
by RUSUB_1:24;

end;
let W1, W2 be Subspace of V;

func W1 + 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 the carrier of it = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def1 defines + RUSUB_2:def 1 :

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for b_{4} being strict Subspace of V holds

( b_{4} = W1 + W2 iff the carrier of b_{4} = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } );

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for b

( b

definition

let V be RealUnitarySpace;

let W1, W2 be Subspace of V;

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

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

b_{1} = b_{2}
by RUSUB_1:24;

end;
let W1, W2 be Subspace of V;

func W1 /\ W2 -> strict Subspace of V means :Def2: :: RUSUB_2:def 2

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

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

ex b

proof end;

uniqueness for b

b

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

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for b_{4} being strict Subspace of V holds

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

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for b

( b

theorem Th1: :: RUSUB_2:1

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for x being object holds

( x in W1 + W2 iff ex v1, v2 being VECTOR of V st

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

for W1, W2 being Subspace of V

for x being object holds

( x in W1 + W2 iff ex v1, v2 being VECTOR of V st

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

proof 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

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 end;

theorem Th3: :: RUSUB_2:3

for V being RealUnitarySpace

for W1, W2 being Subspace of V

for x being object holds

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

for W1, W2 being Subspace of V

for x being object holds

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

proof end;

Lm1: for V being RealUnitarySpace

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

proof 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 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 end;

theorem :: RUSUB_2:4

theorem :: RUSUB_2:5

theorem Th6: :: RUSUB_2:6

for V being RealUnitarySpace

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

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

proof 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 )

for W1, W2 being Subspace of V holds

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

proof 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 )

for W1 being Subspace of V

for W2 being strict Subspace of V holds

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

proof 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 )

for W being strict Subspace of V holds

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

proof 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 #) )

( ((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 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 #) )

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 end;

theorem :: RUSUB_2:12

theorem Th15: :: RUSUB_2:15

for V being RealUnitarySpace

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

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

proof 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 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 )

for W1, W2 being Subspace of V holds

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

proof 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 )

for W2 being Subspace of V

for W1 being strict Subspace of V holds

( W1 is Subspace of W2 iff W1 /\ W2 = W1 )

proof 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 )

for W being Subspace of V holds

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

proof end;

theorem :: RUSUB_2:19

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 )

for W being strict Subspace of V holds

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

proof 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 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;

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 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;

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 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;

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 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;

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 end;

theorem :: RUSUB_2:26

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 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;

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 end;

theorem :: RUSUB_2:28

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

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

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

proof 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 )

for W1, W2 being strict Subspace of V holds

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

proof 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

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 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 )

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 end;

definition

let V be RealUnitarySpace;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict Subspace of V )

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

( x in b_{1} iff x is strict Subspace of V ) ) & ( for x being object holds

( x in b_{2} iff x is strict Subspace of V ) ) holds

b_{1} = b_{2}

end;
func Subspaces V -> set means :Def3: :: RUSUB_2:def 3

for x being object holds

( x in it iff x is strict Subspace of V );

existence for x being object holds

( x in it iff x is strict Subspace of V );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def3 defines Subspaces RUSUB_2:def 3 :

for V being RealUnitarySpace

for b_{2} being set holds

( b_{2} = Subspaces V iff for x being object holds

( x in b_{2} iff x is strict Subspace of V ) );

for V being RealUnitarySpace

for b

( b

( x in b

:: deftheorem 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 ) );

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 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 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 end;

definition

let V be RealUnitarySpace;

let W be Subspace of V;

existence

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

end;
let W be Subspace of V;

existence

ex b

proof end;

:: deftheorem Def5 defines Linear_Compl RUSUB_2:def 5 :

for V being RealUnitarySpace

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

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

for V being RealUnitarySpace

for W, b

( b

registration

let V be RealUnitarySpace;

let W be Subspace of V;

ex b_{1} being Linear_Compl of W st b_{1} is strict

end;
let W be Subspace of V;

cluster non empty V103() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RealUnitarySpace-like for Linear_Compl of W;

existence ex b

proof 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

by Th14, Lm1;

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 by Lm15, Def5;

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

W2 is Linear_Compl of W1 by Lm15, Def5;

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 ) by Def5, Lm15;

for W being Subspace of V

for L being Linear_Compl of W holds

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

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 #) )

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 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 )

for W being Subspace of V

for L being Linear_Compl of W holds

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

proof end;

theorem :: 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;

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 ) by Th10, Th18;

( V is_the_direct_sum_of (0). V, (Omega). V & V is_the_direct_sum_of (Omega). V, (0). V ) by Th10, Th18;

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

for W being Subspace of V

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

proof 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 ) by Th39, Def5;

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

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 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

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 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 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} )

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 end;

theorem :: RUSUB_2:44

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 )

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 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

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 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 ;

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

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

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

b_{1} = b_{2}

end;
let v be VECTOR of V;

let W1, W2 be Subspace of V;

assume A1: V is_the_direct_sum_of W1,W2 ;

func v |-- (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 ( v = (it `1) + (it `2) & it `1 in W1 & it `2 in W2 );

ex b

( v = (b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines |-- 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 b_{5} being Element of [: the carrier of V, the carrier of V:] holds

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

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 b

( b

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

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 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

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 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)

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 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

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 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 )

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 end;

theorem :: RUSUB_2:52

theorem :: RUSUB_2:53

definition

let V be RealUnitarySpace;

ex b_{1} 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

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

for b_{1}, b_{2} 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

b_{1} . (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

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

b_{1} = b_{2}

end;
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 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;

ex b

for A1, A2 being Element of Subspaces V

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def7 defines SubJoin RUSUB_2:def 7 :

for V being RealUnitarySpace

for b_{2} being BinOp of (Subspaces V) holds

( b_{2} = SubJoin V iff for A1, A2 being Element of Subspaces V

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

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

for V being RealUnitarySpace

for b

( b

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

b

definition

let V be RealUnitarySpace;

ex b_{1} 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

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

for b_{1}, b_{2} 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

b_{1} . (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

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

b_{1} = b_{2}

end;
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 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;

ex b

for A1, A2 being Element of Subspaces V

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof end;

:: deftheorem Def8 defines SubMeet RUSUB_2:def 8 :

for V being RealUnitarySpace

for b_{2} being BinOp of (Subspaces V) holds

( b_{2} = SubMeet V iff for A1, A2 being Element of Subspaces V

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

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

for V being RealUnitarySpace

for b

( b

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

b

registration

let V be RealUnitarySpace;

coherence

LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th54;

end;
coherence

LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is Lattice-like by Th54;

theorem Th55: :: RUSUB_2:55

for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is lower-bounded

proof end;

theorem Th56: :: RUSUB_2:56

for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is upper-bounded

proof end;

theorem Th59: :: RUSUB_2:59

for V being RealUnitarySpace holds LattStr(# (Subspaces V),(SubJoin V),(SubMeet V) #) is complemented

proof end;

registration

let V be RealUnitarySpace;

( 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;
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;

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

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

W1 /\ W3 is Subspace of W2 /\ W3

proof end;

theorem :: RUSUB_2:61

theorem :: RUSUB_2:62

theorem :: RUSUB_2:63

:: and coset of a subspace