let V be free Z_Module; :: thesis: for A, B being Subset of V st A c= B & B is Basis of V holds

V is_the_direct_sum_of Lin A, Lin (B \ A)

let A, B be Subset of V; :: thesis: ( A c= B & B is Basis of V implies V is_the_direct_sum_of Lin A, Lin (B \ A) )

assume that

A1: A c= B and

A2: B is Basis of V ; :: thesis: V is_the_direct_sum_of Lin A, Lin (B \ A)

A3: (Lin A) /\ (Lin (B \ A)) = (0). V

V is_the_direct_sum_of Lin A, Lin (B \ A)

let A, B be Subset of V; :: thesis: ( A c= B & B is Basis of V implies V is_the_direct_sum_of Lin A, Lin (B \ A) )

assume that

A1: A c= B and

A2: B is Basis of V ; :: thesis: V is_the_direct_sum_of Lin A, Lin (B \ A)

A3: (Lin A) /\ (Lin (B \ A)) = (0). V

proof

(Omega). V = (Lin A) + (Lin (B \ A))
set U = (Lin A) /\ (Lin (B \ A));

reconsider W = (0). V as strict Submodule of (Lin A) /\ (Lin (B \ A)) by ZMODUL01:54;

for v being Element of ((Lin A) /\ (Lin (B \ A))) holds v in W

end;reconsider W = (0). V as strict Submodule of (Lin A) /\ (Lin (B \ A)) by ZMODUL01:54;

for v being Element of ((Lin A) /\ (Lin (B \ A))) holds v in W

proof

hence
(Lin A) /\ (Lin (B \ A)) = (0). V
by ZMODUL01:149; :: thesis: verum
let v be Element of ((Lin A) /\ (Lin (B \ A))); :: thesis: v in W

A4: B is linearly-independent by A2, VECTSP_7:def 3;

A5: v in (Lin A) /\ (Lin (B \ A)) ;

then v in Lin A by ZMODUL01:94;

then consider l being Linear_Combination of A such that

A6: v = Sum l by ZMODUL02:64;

v in Lin (B \ A) by A5, ZMODUL01:94;

then consider m being Linear_Combination of B \ A such that

A7: v = Sum m by ZMODUL02:64;

A8: 0. V = (Sum l) - (Sum m) by A6, A7, VECTSP_1:19

.= Sum (l - m) by ZMODUL02:55 ;

A9: ( Carrier (l - m) c= (Carrier l) \/ (Carrier m) & A \/ (B \ A) = B ) by A1, XBOOLE_1:45, ZMODUL02:40;

A10: ( Carrier l c= A & Carrier m c= B \ A ) by VECTSP_6:def 4;

then (Carrier l) \/ (Carrier m) c= A \/ (B \ A) by XBOOLE_1:13;

then Carrier (l - m) c= B by A9;

then reconsider n = l - m as Linear_Combination of B by VECTSP_6:def 4;

A misses B \ A by XBOOLE_1:79;

then Carrier n = (Carrier l) \/ (Carrier m) by A10, Th32, XBOOLE_1:64;

then Carrier l = {} by A4, A8;

then l = ZeroLC V by VECTSP_6:def 3;

then Sum l = 0. V by ZMODUL02:19;

hence v in W by A6, ZMODUL02:66; :: thesis: verum

end;A4: B is linearly-independent by A2, VECTSP_7:def 3;

A5: v in (Lin A) /\ (Lin (B \ A)) ;

then v in Lin A by ZMODUL01:94;

then consider l being Linear_Combination of A such that

A6: v = Sum l by ZMODUL02:64;

v in Lin (B \ A) by A5, ZMODUL01:94;

then consider m being Linear_Combination of B \ A such that

A7: v = Sum m by ZMODUL02:64;

A8: 0. V = (Sum l) - (Sum m) by A6, A7, VECTSP_1:19

.= Sum (l - m) by ZMODUL02:55 ;

A9: ( Carrier (l - m) c= (Carrier l) \/ (Carrier m) & A \/ (B \ A) = B ) by A1, XBOOLE_1:45, ZMODUL02:40;

A10: ( Carrier l c= A & Carrier m c= B \ A ) by VECTSP_6:def 4;

then (Carrier l) \/ (Carrier m) c= A \/ (B \ A) by XBOOLE_1:13;

then Carrier (l - m) c= B by A9;

then reconsider n = l - m as Linear_Combination of B by VECTSP_6:def 4;

A misses B \ A by XBOOLE_1:79;

then Carrier n = (Carrier l) \/ (Carrier m) by A10, Th32, XBOOLE_1:64;

then Carrier l = {} by A4, A8;

then l = ZeroLC V by VECTSP_6:def 3;

then Sum l = 0. V by ZMODUL02:19;

hence v in W by A6, ZMODUL02:66; :: thesis: verum

proof

hence
V is_the_direct_sum_of Lin A, Lin (B \ A)
by A3, VECTSP_5:def 4; :: thesis: verum
set U = (Lin A) + (Lin (B \ A));

A11: [#] V c= [#] ((Lin A) + (Lin (B \ A)))

hence (Omega). V = (Lin A) + (Lin (B \ A)) by ZMODUL01:45; :: thesis: verum

end;A11: [#] V c= [#] ((Lin A) + (Lin (B \ A)))

proof

[#] ((Lin A) + (Lin (B \ A))) = [#] V
by A11, VECTSP_4:def 2;
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in [#] V or v in [#] ((Lin A) + (Lin (B \ A))) )

assume v in [#] V ; :: thesis: v in [#] ((Lin A) + (Lin (B \ A)))

then reconsider v = v as Element of V ;

v in Lin B by A2, ZMODUL03:14;

then consider l being Linear_Combination of B such that

A12: v = Sum l by ZMODUL02:64;

set n = l ! (B \ A);

set m = l ! A;

A13: l = (l ! A) + (l ! (B \ A)) by A1, Th27;

ex v1, v2 being Element of V st

( v1 in Lin A & v2 in Lin (B \ A) & v = v1 + v2 )

hence v in [#] ((Lin A) + (Lin (B \ A))) ; :: thesis: verum

end;assume v in [#] V ; :: thesis: v in [#] ((Lin A) + (Lin (B \ A)))

then reconsider v = v as Element of V ;

v in Lin B by A2, ZMODUL03:14;

then consider l being Linear_Combination of B such that

A12: v = Sum l by ZMODUL02:64;

set n = l ! (B \ A);

set m = l ! A;

A13: l = (l ! A) + (l ! (B \ A)) by A1, Th27;

ex v1, v2 being Element of V st

( v1 in Lin A & v2 in Lin (B \ A) & v = v1 + v2 )

proof

then
v in (Lin A) + (Lin (B \ A))
by ZMODUL01:92;
take
Sum (l ! A)
; :: thesis: ex v2 being Element of V st

( Sum (l ! A) in Lin A & v2 in Lin (B \ A) & v = (Sum (l ! A)) + v2 )

take Sum (l ! (B \ A)) ; :: thesis: ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) )

thus ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) ) by A12, A13, ZMODUL02:52, ZMODUL02:64; :: thesis: verum

end;( Sum (l ! A) in Lin A & v2 in Lin (B \ A) & v = (Sum (l ! A)) + v2 )

take Sum (l ! (B \ A)) ; :: thesis: ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) )

thus ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) ) by A12, A13, ZMODUL02:52, ZMODUL02:64; :: thesis: verum

hence v in [#] ((Lin A) + (Lin (B \ A))) ; :: thesis: verum

hence (Omega). V = (Lin A) + (Lin (B \ A)) by ZMODUL01:45; :: thesis: verum