let X be non empty addLoopStr ; :: thesis: for A, B being Subset of X
for l being Linear_Combination of A \/ B st A misses B holds
ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
let A, B be Subset of X; :: thesis: for l being Linear_Combination of A \/ B st A misses B holds
ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
let l be Linear_Combination of A \/ B; :: thesis: ( A misses B implies ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) )
assume A2: A misses B ; :: thesis: ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
consider l1 being Linear_Combination of A such that
A3: ( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) ) by Th8;
consider l2 being Linear_Combination of B such that
A4: ( Carrier l2 = (Carrier l) \ A & ( for x being Element of X st x in Carrier l2 holds
l2 . x = l . x ) ) by Th8;
take l1 ; :: thesis: ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
take l2 ; :: thesis: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
A5: (Carrier l1) \/ (Carrier l2) = (Carrier l) \ (A /\ B) by A3, A4, XBOOLE_1:54;
hence (Carrier l1) \/ (Carrier l2) = Carrier l by A2; :: thesis: ( l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
A6: ( Carrier l1 c= A & Carrier l2 c= B ) by RLVECT_2:def 6;
now :: thesis: for x being Element of X holds l . x = (l1 . x) + (l2 . x)
let x be Element of X; :: thesis: l . b1 = (l1 . b1) + (l2 . b1)
per cases ( x in Carrier l1 or x in Carrier l2 or not x in Carrier l ) by A2, A5, XBOOLE_0:def 3;
suppose A7: x in Carrier l1 ; :: thesis: l . b1 = (l1 . b1) + (l2 . b1)
then not x in Carrier l2 by A2, A6, XBOOLE_0:3;
then ( l1 . x = l . x & l2 . x = 0 ) by A3, A7;
hence l . x = (l1 . x) + (l2 . x) ; :: thesis: verum
end;
suppose A8: x in Carrier l2 ; :: thesis: l . b1 = (l1 . b1) + (l2 . b1)
then not x in Carrier l1 by A2, A6, XBOOLE_0:3;
then ( l1 . x = 0 & l2 . x = l . x ) by A4, A8;
hence l . x = (l1 . x) + (l2 . x) ; :: thesis: verum
end;
suppose A9: not x in Carrier l ; :: thesis: l . b1 = (l1 . b1) + (l2 . b1)
then ( not x in Carrier l1 & not x in Carrier l2 ) by A2, A5, XBOOLE_0:def 3;
then ( l . x = 0 & l1 . x = 0 & l2 . x = 0 ) by A9;
hence l . x = (l1 . x) + (l2 . x) ; :: thesis: verum
end;
end;
end;
hence l = l1 + l2 by RLVECT_2:def 10; :: thesis: ( Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A )
thus ( Carrier l1 = (Carrier l) \ B & Carrier l2 = (Carrier l) \ A ) by A3, A4; :: thesis: verum