let K be Field; 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; 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; ( 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
; 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)
reconsider W19 = W1, W29 = W2 as Subspace of W1 + W2 by VECTSP_5:7;
let B1 be linearly-independent Subset of W1; 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; B1 \/ B2 is linearly-independent Subset of (W1 + W2)
A2:
W2 is Subspace of W1 + W2
by VECTSP_5:7;
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)
;
A4:
W1 is Subspace of W1 + W2
by VECTSP_5:7;
then
the carrier of W1 c= the carrier of (W1 + W2)
by VECTSP_4:def 2;
then
B1 c= the carrier of (W1 + W2)
;
then reconsider B12 = B1 \/ B2, B19 = B1, B29 = B2 as Subset of (W1 + W2) 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 4;
set C =
(Carrier L) /\ B1;
defpred S1[
object ]
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
(W1 + W2) by XBOOLE_1:1;
set D =
(Carrier L) \ B1;
deffunc H1(
object )
-> set =
L . $1;
defpred S2[
object ]
means $1
in (Carrier L) \ B1;
reconsider D =
(Carrier L) \ B1 as
finite Subset of
(W1 + W2) ;
A6:
D c= B29
(0). V = (0). (W1 + W2)
by VECTSP_4:36;
then A8:
W19 /\ W29 = (0). (W1 + W2)
by A1, Th1;
W19 + W29 = W1 + W2
by Th1;
then A9:
W1 + W2 is_the_direct_sum_of W19,
W29
by A8, VECTSP_5:def 4;
A10:
B29 is
linearly-independent
by A2, VECTSP_9:11;
A11:
B19 is
linearly-independent
by A4, VECTSP_9:11;
deffunc H2(
object )
-> Element of the
carrier of
K =
0. K;
A12:
(
0. W1 in W19 &
0. W2 in W29 )
;
consider f being
Function of the
carrier of
(W1 + W2), the
carrier of
K such that A14:
for
x being
object 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(
object )
-> set =
L . $1;
consider g being
Function of the
carrier of
(W1 + W2), the
carrier of
K such that A16:
for
x being
object 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:8;
for
u being
Vector of
(W1 + W2) 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 1;
A17:
Carrier g c= D
then
Carrier g c= B29
by A6;
then reconsider g =
g as
Linear_Combination of
B29 by VECTSP_6:def 4;
reconsider f =
f as
Element of
Funcs ( the
carrier of
(W1 + W2), the
carrier of
K)
by FUNCT_2:8;
for
u being
Vector of
(W1 + W2) 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 1;
A19:
Carrier f c= B19
then reconsider f =
f as
Linear_Combination of
B19 by VECTSP_6:def 4;
ex
f1 being
Linear_Combination of
W19 st
(
Carrier f1 = Carrier f &
Sum f = Sum f1 )
by A19, VECTSP_9:9, XBOOLE_1:1;
then A21:
Sum f in W19
;
A22:
L = f + g
then A31:
Sum L = (Sum f) + (Sum g)
by VECTSP_6:44;
Carrier g c= B2
by A17, A6;
then
ex
g1 being
Linear_Combination of
W29 st
(
Carrier g1 = Carrier g &
Sum g = Sum g1 )
by VECTSP_9:9, XBOOLE_1:1;
then A32:
Sum g in W29
;
A33:
(
0. (W1 + W2) = 0. W19 &
0. (W1 + W2) = 0. W29 )
by VECTSP_4:11;
then
Sum f = 0. (W1 + W2)
by A31, A21, A32, A9, A12, A5, VECTSP_5:48;
then A34:
Carrier f = {}
by A11;
Sum g = 0. (W1 + W2)
by A31, A21, A32, A9, A33, A12, A5, VECTSP_5:48;
then A35:
Carrier g = {}
by A10;
{} \/ {} = {}
;
hence
Carrier L = {}
by A22, A34, A35, VECTSP_6:23, XBOOLE_1:3;
verum
end;
hence
B1 \/ B2 is linearly-independent Subset of (W1 + W2)
; verum