defpred S1[ Nat] means for W1, W2 being free finite-rank Subspace of V st rank W1 = V holds
W1 + W2 is free finite-rank Subspace of V;
A1:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A21:
S1[
n]
;
S1[n + 1]
let W1,
W2 be
free finite-rank Subspace of
V;
( rank W1 = n + 1 implies W1 + W2 is free finite-rank Subspace of V )
assume A22:
rank W1 = n + 1
;
W1 + W2 is free finite-rank Subspace of V
reconsider W1s =
(Omega). W1 as
strict Subspace of
V by ZMODUL01:42;
reconsider W2s =
(Omega). W2 as
strict Subspace of
V by ZMODUL01:42;
consider I being
finite Subset of
W1 such that C30:
I is
Basis of
W1
by ZMODUL03:def 3;
reconsider I =
I as
Basis of
W1 by C30;
C31:
(
card I <> 0 &
card I = n + 1 )
by A22, ZMODUL03:def 5;
then
I <> {}
;
then consider u being
object such that C32:
u in I
by XBOOLE_0:7;
reconsider u0 =
u as
Vector of
W1 by C32;
(
I c= the
carrier of
W1 & the
carrier of
W1 c= the
carrier of
V )
by VECTSP_4:def 2;
then reconsider u =
u as
Vector of
V by C32;
D33:
(
I \ {u} c= I &
I c= the
carrier of
W1 )
by XBOOLE_1:36;
reconsider J =
I \ {u} as
finite Subset of
W1 ;
(card I) - (card {u}) = (n + 1) - 1
by C31, CARD_1:30;
then C34:
card J = n
by C32, ZFMISC_1:31, CARD_2:44;
D34:
J is
linearly-independent
by D33, VECTSP_7:def 3, ZMODUL02:56;
reconsider W10 =
Lin J as
free finite-rank Subspace of
V by ZMODUL01:42;
reconsider W10s =
(Omega). W10 as
strict Subspace of
V ;
for
x being
object st
x in J holds
x in the
carrier of
W10
then
J c= the
carrier of
W10
;
then reconsider J0 =
J as
linearly-independent Subset of
W10 by D34, ZMODUL03:16;
(
W10s = Lin J0 &
Lin J0 = Lin J )
by ZMODUL03:20;
then
J0 is
Basis of
W10
by VECTSP_7:def 3;
then
rank W10 = n
by C34, ZMODUL03:def 5;
then reconsider W3 =
W10 + W2 as
free finite-rank Subspace of
V by A21;
R2:
Lin {u0} = Lin {u}
by ZMODUL03:20;
W1 is_the_direct_sum_of Lin J,
Lin {u0}
by C32, ZMODUL04:33;
then Q2:
W1s = W10s + (Lin {u})
by LMThSumMod2, R2;
W1 + W2 =
W1s + W2s
by ZMODUL04:22
.=
(Lin {u}) + (W10s + W2s)
by ZMODUL01:96, Q2
.=
(Lin {u}) + W3
by ZMODUL04:22
;
hence
W1 + W2 is
free finite-rank Subspace of
V
;
verum
end;
A3:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
set rk = rank U1;
S1[ rank U1]
by A3;
hence
U1 + U2 is free
; verum