let V be free Z_Module; :: thesis: for I being Basis of V

for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let I be Basis of V; :: thesis: for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let v be Vector of V; :: thesis: ( v in I implies V is_the_direct_sum_of Lin (I \ {v}), Lin {v} )

assume A1: v in I ; :: thesis: V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

I = (I \ {v}) \/ {v} by A1, XBOOLE_1:45, ZFMISC_1:31;

then Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;

then A3: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (Lin (I \ {v})) + (Lin {v}) by VECTSP_7:def 3;

the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) = {(0. V)}

hence V is_the_direct_sum_of Lin (I \ {v}), Lin {v} by A3, VECTSP_5:def 4; :: thesis: verum

for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let I be Basis of V; :: thesis: for v being Vector of V st v in I holds

V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

let v be Vector of V; :: thesis: ( v in I implies V is_the_direct_sum_of Lin (I \ {v}), Lin {v} )

assume A1: v in I ; :: thesis: V is_the_direct_sum_of Lin (I \ {v}), Lin {v}

I = (I \ {v}) \/ {v} by A1, XBOOLE_1:45, ZFMISC_1:31;

then Lin I = (Lin (I \ {v})) + (Lin {v}) by ZMODUL02:72;

then A3: ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = (Lin (I \ {v})) + (Lin {v}) by VECTSP_7:def 3;

the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) = {(0. V)}

proof

then
(Lin (I \ {v})) /\ (Lin {v}) = (0). V
by VECTSP_4:def 3, VECTSP_5:def 2;
assume B1:
the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) <> {(0. V)}
; :: thesis: contradiction

0. V in (Lin (I \ {v})) /\ (Lin {v}) by ZMODUL01:33;

then 0. V in the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) by VECTSP_5:def 2;

then {(0. V)} c< the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) by B1, ZFMISC_1:31;

then consider x being object such that

B2: x in the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) and

B3: not x in {(0. V)} by XBOOLE_0:6;

B4: x <> 0. V by B3, TARSKI:def 1;

B5: x in (Lin (I \ {v})) /\ (Lin {v}) by B2, VECTSP_5:def 2;

then x in V by ZMODUL01:24;

then reconsider x = x as Vector of V ;

x in Lin (I \ {v}) by B5, VECTSP_5:3;

then consider lx1 being Linear_Combination of I \ {v} such that

B6: x = Sum lx1 by ZMODUL02:64;

B7: Carrier lx1 <> {} by B4, B6, ZMODUL02:23;

B8: Carrier lx1 c= I \ {v} by VECTSP_6:def 4;

x in Lin {v} by B5, VECTSP_5:3;

then consider lx2 being Linear_Combination of {v} such that

B9: - x = Sum lx2 by ZMODUL01:38, ZMODUL02:64;

B11: Carrier lx2 c= {v} by VECTSP_6:def 4;

reconsider llx1 = lx1 as Linear_Combination of I by XBOOLE_1:36, ZMODUL02:10;

reconsider llx2 = lx2 as Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;

Carrier lx1 misses Carrier lx2 by B8, B11, XBOOLE_1:64, XBOOLE_1:79;

then (Carrier lx1) /\ (Carrier lx2) = {} ;

then B12: Carrier (llx1 + llx2) = (Carrier llx1) \/ (Carrier llx2) by ThCarrier1;

B13: (Sum llx1) + (Sum llx2) = 0. V by B6, B9, RLVECT_1:5;

reconsider llx = llx1 + llx2 as Linear_Combination of I by ZMODUL02:27;

Sum llx = 0. V by B13, ZMODUL02:52;

hence contradiction by B7, B12, VECTSP_7:def 1, VECTSP_7:def 3; :: thesis: verum

end;0. V in (Lin (I \ {v})) /\ (Lin {v}) by ZMODUL01:33;

then 0. V in the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) by VECTSP_5:def 2;

then {(0. V)} c< the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) by B1, ZFMISC_1:31;

then consider x being object such that

B2: x in the carrier of (Lin (I \ {v})) /\ the carrier of (Lin {v}) and

B3: not x in {(0. V)} by XBOOLE_0:6;

B4: x <> 0. V by B3, TARSKI:def 1;

B5: x in (Lin (I \ {v})) /\ (Lin {v}) by B2, VECTSP_5:def 2;

then x in V by ZMODUL01:24;

then reconsider x = x as Vector of V ;

x in Lin (I \ {v}) by B5, VECTSP_5:3;

then consider lx1 being Linear_Combination of I \ {v} such that

B6: x = Sum lx1 by ZMODUL02:64;

B7: Carrier lx1 <> {} by B4, B6, ZMODUL02:23;

B8: Carrier lx1 c= I \ {v} by VECTSP_6:def 4;

x in Lin {v} by B5, VECTSP_5:3;

then consider lx2 being Linear_Combination of {v} such that

B9: - x = Sum lx2 by ZMODUL01:38, ZMODUL02:64;

B11: Carrier lx2 c= {v} by VECTSP_6:def 4;

reconsider llx1 = lx1 as Linear_Combination of I by XBOOLE_1:36, ZMODUL02:10;

reconsider llx2 = lx2 as Linear_Combination of I by A1, ZFMISC_1:31, ZMODUL02:10;

Carrier lx1 misses Carrier lx2 by B8, B11, XBOOLE_1:64, XBOOLE_1:79;

then (Carrier lx1) /\ (Carrier lx2) = {} ;

then B12: Carrier (llx1 + llx2) = (Carrier llx1) \/ (Carrier llx2) by ThCarrier1;

B13: (Sum llx1) + (Sum llx2) = 0. V by B6, B9, RLVECT_1:5;

reconsider llx = llx1 + llx2 as Linear_Combination of I by ZMODUL02:27;

Sum llx = 0. V by B13, ZMODUL02:52;

hence contradiction by B7, B12, VECTSP_7:def 1, VECTSP_7:def 3; :: thesis: verum

hence V is_the_direct_sum_of Lin (I \ {v}), Lin {v} by A3, VECTSP_5:def 4; :: thesis: verum