let K be Field; for V being VectSp of
for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being linearly-independent Subset of
for B2 being linearly-independent Subset of holds B1 \/ B2 is linearly-independent Subset of
let V be VectSp of ; for W1, W2 being Subspace of V st W1 /\ W2 = (0). V holds
for B1 being linearly-independent Subset of
for B2 being linearly-independent Subset of holds B1 \/ B2 is linearly-independent Subset of
let W1, W2 be Subspace of V; ( W1 /\ W2 = (0). V implies for B1 being linearly-independent Subset of
for B2 being linearly-independent Subset of holds B1 \/ B2 is linearly-independent Subset of )
assume A1:
W1 /\ W2 = (0). V
; for B1 being linearly-independent Subset of
for B2 being linearly-independent Subset of holds B1 \/ B2 is linearly-independent Subset of
reconsider W1' = W1, W2' = W2 as Subspace of W1 + W2 by VECTSP_5:11;
let B1 be linearly-independent Subset of ; for B2 being linearly-independent Subset of holds B1 \/ B2 is linearly-independent Subset of
let B2 be linearly-independent Subset of ; B1 \/ B2 is linearly-independent Subset of
A2:
W2 is Subspace of W1 + W2
by VECTSP_5:11;
then
the carrier of W2 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then A3:
B2 c= the carrier of (W1 + W2)
by XBOOLE_1:1;
A4:
W1 is Subspace of W1 + W2
by VECTSP_5:11;
then
the carrier of W1 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
B1 c= the carrier of (W1 + W2)
by XBOOLE_1:1;
then reconsider B12 = B1 \/ B2, B1' = B1, B2' = B2 as Subset of by A3, XBOOLE_1:8;
B12 is linearly-independent
proof
let L be
Linear_Combination of
B12;
VECTSP_7:def 1 ( not Sum L = 0. (W1 + W2) or Carrier L = {} )
assume
Sum L = 0. (W1 + W2)
;
Carrier L = {}
then A5:
Sum L = (0. (W1 + W2)) + (0. (W1 + W2))
by RLVECT_1:def 7;
set C =
(Carrier L) /\ B1;
defpred S1[
set ]
means $1
in (Carrier L) /\ B1;
(Carrier L) /\ B1 c= Carrier L
by XBOOLE_1:17;
then reconsider C =
(Carrier L) /\ B1 as
finite Subset of
by XBOOLE_1:1;
set D =
(Carrier L) \ B1;
deffunc H1(
set )
-> set =
L . $1;
defpred S2[
set ]
means $1
in (Carrier L) \ B1;
reconsider D =
(Carrier L) \ B1 as
finite Subset of ;
A6:
D c= B2'
(0). V = (0). (W1 + W2)
by VECTSP_4:47;
then A8:
W1' /\ W2' = (0). (W1 + W2)
by A1, Th1;
W1' + W2' = W1 + W2
by Th1;
then A9:
W1 + W2 is_the_direct_sum_of W1',
W2'
by A8, VECTSP_5:def 4;
A10:
B2' is
linearly-independent
by A2, VECTSP_9:15;
A11:
B1' is
linearly-independent
by A4, VECTSP_9:15;
deffunc H2(
set )
-> Element of the
carrier of
K =
0. K;
A12:
(
0. W1 in W1' &
0. W2 in W2' )
by STRUCT_0:def 5;
consider f being
Function of the
carrier of
(W1 + W2),the
carrier of
K such that A14:
for
x being
set st
x in the
carrier of
(W1 + W2) holds
( (
S1[
x] implies
f . x = H1(
x) ) & ( not
S1[
x] implies
f . x = H2(
x) ) )
from FUNCT_2:sch 5(A13);
deffunc H3(
set )
-> set =
L . $1;
consider g being
Function of the
carrier of
(W1 + W2),the
carrier of
K such that A16:
for
x being
set st
x in the
carrier of
(W1 + W2) holds
( (
S2[
x] implies
g . x = H3(
x) ) & ( not
S2[
x] implies
g . x = H2(
x) ) )
from FUNCT_2:sch 5(A15);
reconsider g =
g as
Element of
Funcs the
carrier of
(W1 + W2),the
carrier of
K by FUNCT_2:11;
for
u being
Vector of st not
u in D holds
g . u = 0. K
by A16;
then reconsider g =
g as
Linear_Combination of
W1 + W2 by VECTSP_6:def 4;
A17:
Carrier g c= D
then
Carrier g c= B2'
by A6, XBOOLE_1:1;
then reconsider g =
g as
Linear_Combination of
B2' by VECTSP_6:def 7;
reconsider f =
f as
Element of
Funcs the
carrier of
(W1 + W2),the
carrier of
K by FUNCT_2:11;
for
u being
Vector of st not
u in C holds
f . u = 0. K
by A14;
then reconsider f =
f as
Linear_Combination of
W1 + W2 by VECTSP_6:def 4;
A19:
Carrier f c= B1'
then reconsider f =
f as
Linear_Combination of
B1' by VECTSP_6:def 7;
ex
f1 being
Linear_Combination of
W1' st
(
Carrier f1 = Carrier f &
Sum f = Sum f1 )
by A19, VECTSP_9:13, XBOOLE_1:1;
then A21:
Sum f in W1'
by STRUCT_0:def 5;
A22:
L = f + g
then A31:
Sum L = (Sum f) + (Sum g)
by VECTSP_6:77;
Carrier g c= B2
by A17, A6, XBOOLE_1:1;
then
ex
g1 being
Linear_Combination of
W2' st
(
Carrier g1 = Carrier g &
Sum g = Sum g1 )
by VECTSP_9:13, XBOOLE_1:1;
then A32:
Sum g in W2'
by STRUCT_0:def 5;
A33:
(
0. (W1 + W2) = 0. W1' &
0. (W1 + W2) = 0. W2' )
by VECTSP_4:19;
then
Sum f = 0. (W1 + W2)
by A31, A21, A32, A9, A12, A5, VECTSP_5:58;
then A34:
Carrier f = {}
by A11, VECTSP_7:def 1;
Sum g = 0. (W1 + W2)
by A31, A21, A32, A9, A33, A12, A5, VECTSP_5:58;
then A35:
Carrier g = {}
by A10, VECTSP_7:def 1;
{} \/ {} = {}
;
hence
Carrier L = {}
by A22, A34, A35, VECTSP_6:51, XBOOLE_1:3;
verum
end;
hence
B1 \/ B2 is linearly-independent Subset of
; verum