let V be Z_Module; for W being free Subspace of V
for I being Subset of V
for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let W be free Subspace of V; for I being Subset of V
for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let I be Subset of V; for v being Vector of V st I is linearly-independent & Lin I = (Omega). W & v in I holds
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
let v be Vector of V; ( I is linearly-independent & Lin I = (Omega). W & v in I implies ( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V ) )
assume A1:
( I is linearly-independent & Lin I = (Omega). W & v in I )
; ( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
A2: (I \ {v}) \/ {v} =
I \/ {v}
by XBOOLE_1:39
.=
I
by A1, ZFMISC_1:40
;
A3:
I \ {v} is linearly-independent
by A1, ZMODUL02:56, XBOOLE_1:36;
A4:
not v is torsion
by A1, ThLIV1;
(Lin (I \ {v})) /\ (Lin {v}) = (0). V
proof
assume
(Lin (I \ {v})) /\ (Lin {v}) <> (0). V
;
contradiction
then consider x being
Vector of
V such that B2:
(
x in (Lin (I \ {v})) /\ (Lin {v}) &
x <> 0. V )
by ZMODUL04:24;
x in Lin (I \ {v})
by B2, ZMODUL01:94;
then consider lx1 being
Linear_Combination of
I \ {v} such that B3:
x = Sum lx1
by ZMODUL02:64;
B4:
Carrier lx1 <> {}
by B2, B3, ZMODUL02:23;
reconsider llx1 =
lx1 as
Linear_Combination of
I by XBOOLE_1:36, ZMODUL02:10;
x in Lin {v}
by B2, ZMODUL01:94;
then consider lx2 being
Linear_Combination of
{v} such that B5:
- x = Sum lx2
by ZMODUL01:38, ZMODUL02:64;
reconsider llx2 =
lx2 as
Linear_Combination of
I by A1, ZFMISC_1:31, ZMODUL02:10;
B6:
Carrier lx1 c= I \ {v}
by VECTSP_6:def 4;
Carrier lx2 c= {v}
by VECTSP_6:def 4;
then
Carrier lx1 misses Carrier lx2
by B6, XBOOLE_1:64, XBOOLE_1:79;
then
(Carrier lx1) /\ (Carrier lx2) = {}
by XBOOLE_0:def 7;
then B7:
Carrier (llx1 + llx2) = (Carrier llx1) \/ (Carrier llx2)
by ZMODUL04:25;
B8:
(Sum llx1) + (Sum llx2) = 0. V
by B3, B5, RLVECT_1:5;
reconsider llx =
llx1 + llx2 as
Linear_Combination of
I by ZMODUL02:27;
Sum llx = 0. V
by B8, ZMODUL02:52;
hence
contradiction
by A1, B4, B7;
verum
end;
hence
( (Omega). W = (Lin (I \ {v})) + (Lin {v}) & (Lin (I \ {v})) /\ (Lin {v}) = (0). V & Lin (I \ {v}) is free & Lin {v} is free & v <> 0. V )
by A2, A3, A4, A1, ZMODUL02:72, ThnTV4; verum