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