let V be torsion-free Z_Module; for W being free finite-rank Subspace of V
for v, u being Vector of V st v <> 0. V & u <> 0. V & W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V & (Lin {u}) /\ (Lin {v}) = (0). V holds
ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) )
let W be free finite-rank Subspace of V; for v, u being Vector of V st v <> 0. V & u <> 0. V & W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V & (Lin {u}) /\ (Lin {v}) = (0). V holds
ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) )
let v, u be Vector of V; ( v <> 0. V & u <> 0. V & W /\ (Lin {v}) = (0). V & (W + (Lin {u})) /\ (Lin {v}) <> (0). V & (Lin {u}) /\ (Lin {v}) = (0). V implies ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) ) )
assume that
A1:
( v <> 0. V & u <> 0. V )
and
A2:
W /\ (Lin {v}) = (0). V
and
A3:
( (W + (Lin {u})) /\ (Lin {v}) <> (0). V & (Lin {u}) /\ (Lin {v}) = (0). V )
; ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) )
consider x being Vector of V such that
A4:
( x in (W + (Lin {u})) /\ (Lin {v}) & x <> 0. V )
by A3, ZMODUL04:24;
x in W + (Lin {u})
by A4, ZMODUL01:94;
then consider x1, x2 being Vector of V such that
A6:
( x1 in W & x2 in Lin {u} & x = x1 + x2 )
by ZMODUL01:92;
A7:
x in Lin {v}
by A4, ZMODUL01:94;
consider iv being Element of INT.Ring such that
A9:
x = iv * v
by A7, ThLin1;
A10:
iv <> 0
by A4, A9, ZMODUL01:1;
consider iu2 being Element of INT.Ring such that
A11:
x2 = iu2 * u
by A6, ThLin1;
consider iiv, iiu2 being Integer such that
A13:
( iv = (iv gcd iu2) * iiv & iu2 = (iv gcd iu2) * iiu2 & iiv,iiu2 are_coprime )
by A10, INT_2:23;
reconsider iiv = iiv, iiu2 = iiu2 as Element of INT.Ring by INT_1:def 2;
consider Jv, Ju2 being Element of INT.Ring such that
A14:
(iiv * Jv) + (iiu2 * Ju2) = 1
by A13, LmGCD;
reconsider jv = Jv, ju2 = Ju2 as Element of INT.Ring ;
a14:
(iiv * jv) + (iiu2 * ju2) = 1. INT.Ring
by A14;
A15: x - x2 =
x1 + (x2 - x2)
by RLVECT_1:def 3, A6
.=
x1 + (0. V)
by RLVECT_1:15
.=
x1
;
set w1 = (iiv * v) - (iiu2 * u);
set w2 = (jv * u) + (ju2 * v);
A16:
(iiv * v) - (iiu2 * u) <> 0. V
proof
assume
(iiv * v) - (iiu2 * u) = 0. V
;
contradiction
then B1:
iiv * v = iiu2 * u
by RLVECT_1:21;
B2:
iiv * v in Lin {v}
by ZMODUL01:37, ThLin2;
iiv * v in Lin {u}
by B1, ZMODUL01:37, ThLin2;
then B3:
iiv * v in (Lin {u}) /\ (Lin {v})
by B2, ZMODUL01:94;
iiv <> 0. INT.Ring
by A13, A4, A9, ZMODUL01:1;
hence
contradiction
by A3, B3, ZMODUL02:66, A1, ZMODUL01:def 7;
verum
end;
reconsider igu = iv gcd iu2 as Element of INT.Ring by INT_1:def 2;
a13:
( iv = igu * iiv & iu2 = igu * iiu2 )
by A13;
AX1:
igu * ((iiv * v) - (iiu2 * u)) in W
AX2:
iv gcd iu2 <> 0. INT.Ring
by A10, INT_2:5;
A17:
W /\ (Lin {((iiv * v) - (iiu2 * u))}) <> (0). V
A18:
u = (iiv * ((jv * u) + (ju2 * v))) - (ju2 * ((iiv * v) - (iiu2 * u)))
A19:
v = (jv * ((iiv * v) - (iiu2 * u))) + (iiu2 * ((jv * u) + (ju2 * v)))
A20:
u in (Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))})
A21:
v in (Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))})
A22:
(iiv * v) - (iiu2 * u) in (Lin {u}) + (Lin {v})
A23:
(jv * u) + (ju2 * v) in (Lin {u}) + (Lin {v})
A24:
for x being object st x in (W + (Lin {u})) + (Lin {v}) holds
x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))})
proof
let x be
object ;
( x in (W + (Lin {u})) + (Lin {v}) implies x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))}) )
assume
x in (W + (Lin {u})) + (Lin {v})
;
x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))})
then consider xx,
x3 being
Vector of
V such that B1:
(
xx in W + (Lin {u}) &
x3 in Lin {v} &
x = xx + x3 )
by ZMODUL01:92;
consider x1,
x2 being
Vector of
V such that B2:
(
x1 in W &
x2 in Lin {u} &
xx = x1 + x2 )
by B1, ZMODUL01:92;
consider ix2 being
Element of
INT.Ring such that B3:
x2 = ix2 * u
by B2, ThLin1;
consider ix3 being
Element of
INT.Ring such that B4:
x3 = ix3 * v
by B1, ThLin1;
B5:
x2 in (Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))})
by A20, B3, ZMODUL01:37;
x3 in (Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))})
by A21, B4, ZMODUL01:37;
then
x2 + x3 in (Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))})
by B5, ZMODUL01:36;
then
x1 + (x2 + x3) in W + ((Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))}))
by B2, ZMODUL01:92;
then
xx + x3 in W + ((Lin {((iiv * v) - (iiu2 * u))}) + (Lin {((jv * u) + (ju2 * v))}))
by B2, RLVECT_1:def 3;
hence
x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))})
by B1, ZMODUL01:96;
verum
end;
for x being object st x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))}) holds
x in (W + (Lin {u})) + (Lin {v})
proof
let x be
object ;
( x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))}) implies x in (W + (Lin {u})) + (Lin {v}) )
assume
x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))})
;
x in (W + (Lin {u})) + (Lin {v})
then consider xx,
x3 being
Vector of
V such that B1:
(
xx in W + (Lin {((iiv * v) - (iiu2 * u))}) &
x3 in Lin {((jv * u) + (ju2 * v))} &
x = xx + x3 )
by ZMODUL01:92;
consider x1,
x2 being
Vector of
V such that B2:
(
x1 in W &
x2 in Lin {((iiv * v) - (iiu2 * u))} &
xx = x1 + x2 )
by B1, ZMODUL01:92;
consider ix2 being
Element of
INT.Ring such that B3:
x2 = ix2 * ((iiv * v) - (iiu2 * u))
by B2, ThLin1;
consider ix3 being
Element of
INT.Ring such that B4:
x3 = ix3 * ((jv * u) + (ju2 * v))
by B1, ThLin1;
B5:
x2 in (Lin {u}) + (Lin {v})
by A22, B3, ZMODUL01:37;
x3 in (Lin {u}) + (Lin {v})
by A23, B4, ZMODUL01:37;
then
x2 + x3 in (Lin {u}) + (Lin {v})
by B5, ZMODUL01:36;
then
x1 + (x2 + x3) in W + ((Lin {u}) + (Lin {v}))
by B2, ZMODUL01:92;
then
xx + x3 in W + ((Lin {u}) + (Lin {v}))
by B2, RLVECT_1:def 3;
hence
x in (W + (Lin {u})) + (Lin {v})
by B1, ZMODUL01:96;
verum
end;
then
for x being Vector of V holds
( x in (W + (Lin {u})) + (Lin {v}) iff x in (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))}) )
by A24;
then A25:
(W + (Lin {u})) + (Lin {v}) = (W + (Lin {((iiv * v) - (iiu2 * u))})) + (Lin {((jv * u) + (ju2 * v))})
by ZMODUL01:46;
A26:
(jv * u) + (ju2 * v) <> 0. V
(W + (Lin {((iiv * v) - (iiu2 * u))})) /\ (Lin {((jv * u) + (ju2 * v))}) = (0). V
proof
assume
(W + (Lin {((iiv * v) - (iiu2 * u))})) /\ (Lin {((jv * u) + (ju2 * v))}) <> (0). V
;
contradiction
then consider wx being
Vector of
V such that B2:
(
wx in (W + (Lin {((iiv * v) - (iiu2 * u))})) /\ (Lin {((jv * u) + (ju2 * v))}) &
wx <> 0. V )
by ZMODUL04:24;
wx in W + (Lin {((iiv * v) - (iiu2 * u))})
by B2, ZMODUL01:94;
then consider wx1,
wx2 being
Vector of
V such that B3:
(
wx1 in W &
wx2 in Lin {((iiv * v) - (iiu2 * u))} &
wx = wx1 + wx2 )
by ZMODUL01:92;
consider iwx1 being
Element of
INT.Ring such that B4:
wx2 = iwx1 * ((iiv * v) - (iiu2 * u))
by B3, ThLin1;
reconsider igu =
iv gcd iu2 as
Element of
INT.Ring by INT_1:def 2;
B5:
igu * wx in W
wx in Lin {((jv * u) + (ju2 * v))}
by B2, ZMODUL01:94;
then consider iwx2 being
Element of
INT.Ring such that B6:
wx = iwx2 * ((jv * u) + (ju2 * v))
by ThLin1;
B7:
iwx2 <> 0
by B2, B6, ZMODUL01:1;
ex
wiu1,
wiu2 being
Vector of
V st
(
iu2 * ((jv * u) + (ju2 * v)) = wiu1 + wiu2 &
wiu1 in W &
wiu2 = igu * v )
then consider wiu1,
wiu2 being
Vector of
V such that B8:
(
iu2 * ((jv * u) + (ju2 * v)) = wiu1 + wiu2 &
wiu1 in W &
wiu2 = igu * v )
;
B9:
iu2 * wx =
(iu2 * iwx2) * ((jv * u) + (ju2 * v))
by VECTSP_1:def 16, B6
.=
iwx2 * (iu2 * ((jv * u) + (ju2 * v)))
by VECTSP_1:def 16
.=
(iwx2 * wiu1) + (iwx2 * (igu * v))
by VECTSP_1:def 14, B8
.=
(iwx2 * wiu1) + ((iwx2 * igu) * v)
by VECTSP_1:def 16
;
iu2 * wx = iiu2 * (igu * wx)
by VECTSP_1:def 16, a13;
then B10:
iu2 * wx in W
by B5, ZMODUL01:37;
iwx2 * wiu1 in W
by B8, ZMODUL01:37;
then B11:
(iu2 * wx) - (iwx2 * wiu1) in W
by B10, ZMODUL01:39;
B12:
(iu2 * wx) - (iwx2 * wiu1) =
((iwx2 * wiu1) - (iwx2 * wiu1)) + ((iwx2 * igu) * v)
by RLVECT_1:def 3, B9
.=
(0. V) + ((iwx2 * igu) * v)
by RLVECT_1:15
.=
(iwx2 * igu) * v
;
(iwx2 * igu) * v in Lin {v}
by ZMODUL01:37, ThLin2;
then
(iwx2 * igu) * v in W /\ (Lin {v})
by B12, ZMODUL01:94, B11;
hence
contradiction
by A2, ZMODUL02:66, A1, ZMODUL01:def 7, AX2, B7;
verum
end;
hence
ex w1, w2 being Vector of V st
( w1 <> 0. V & w2 <> 0. V & (W + (Lin {u})) + (Lin {v}) = (W + (Lin {w1})) + (Lin {w2}) & W /\ (Lin {w1}) <> (0). V & (W + (Lin {w1})) /\ (Lin {w2}) = (0). V & u in (Lin {w1}) + (Lin {w2}) & v in (Lin {w1}) + (Lin {w2}) & w1 in (Lin {u}) + (Lin {v}) & w2 in (Lin {u}) + (Lin {v}) )
by A16, A17, A20, A21, A22, A23, A25, A26; verum