let V be free Z_Module; 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; 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; ( v in I implies V is_the_direct_sum_of Lin (I \ {v}), Lin {v} )
assume A1:
v in I
; 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
assume B1:
the
carrier of
(Lin (I \ {v})) /\ the
carrier of
(Lin {v}) <> {(0. V)}
;
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;
verum
end;
then
(Lin (I \ {v})) /\ (Lin {v}) = (0). V
by VECTSP_4:def 3, VECTSP_5:def 2;
hence
V is_the_direct_sum_of Lin (I \ {v}), Lin {v}
by A3, VECTSP_5:def 4; verum