let K be Field; for V1, V2 being VectSp of K
for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let V1, V2 be VectSp of K; for A, B being Subset of V1
for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let A, B be Subset of V1; for L being Linear_Combination of V1 st Carrier L c= A \/ B & Sum L = 0. V1 holds
for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
let L be Linear_Combination of V1; ( Carrier L c= A \/ B & Sum L = 0. V1 implies for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A )
assume that
A1:
Carrier L c= A \/ B
and
A2:
Sum L = 0. V1
; for f being additive homogeneous Function of V1,V2 st f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} holds
Carrier L c= A
consider F being FinSequence of V1 such that
A3:
F is one-to-one
and
A4:
rng F = Carrier L
and
A5:
0. V1 = Sum (L (#) F)
by A2, VECTSP_6:def 6;
let f be additive homogeneous Function of V1,V2; ( f | B is one-to-one & f .: B is linearly-independent Subset of V2 & f .: A c= {(0. V2)} implies Carrier L c= A )
assume that
A6:
f | B is one-to-one
and
A7:
f .: B is linearly-independent Subset of V2
and
A8:
f .: A c= {(0. V2)}
; Carrier L c= A
per cases
( dom F = {} or dom F <> {} )
;
suppose
dom F <> {}
;
Carrier L c= Athen reconsider D =
dom F as non
empty finite set ;
set C =
Carrier L;
set FA =
F " ((Carrier L) /\ A);
set FB =
F " ((Carrier L) /\ B);
set SS =
(Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)));
A9:
(Carrier L) /\ ((Carrier L) /\ B) = (Carrier L) /\ B
by XBOOLE_1:18, XBOOLE_1:28;
rng F c= the
carrier of
V1
by RELAT_1:def 19;
then reconsider F9 =
F as
Function of
D, the
carrier of
V1 by FUNCT_2:2;
A10:
D = Seg (len F)
by FINSEQ_1:def 3;
then A11:
Sgm (F " ((Carrier L) /\ A)) is
one-to-one
by FINSEQ_3:92, RELAT_1:132;
A12:
(
len (Sgm (F " ((Carrier L) /\ A))) = card (F " ((Carrier L) /\ A)) &
len (Sgm (F " ((Carrier L) /\ B))) = card (F " ((Carrier L) /\ B)) )
by A10, FINSEQ_3:39, RELAT_1:132;
A13:
Sgm (F " ((Carrier L) /\ B)) is
one-to-one
by A10, FINSEQ_3:92, RELAT_1:132;
A14:
F " ((Carrier L) /\ B) c= D
by RELAT_1:132;
then A15:
rng (Sgm (F " ((Carrier L) /\ B))) = F " ((Carrier L) /\ B)
by A10, FINSEQ_1:def 13;
A16:
F " ((Carrier L) /\ A) c= D
by RELAT_1:132;
then A17:
rng (Sgm (F " ((Carrier L) /\ A))) = F " ((Carrier L) /\ A)
by A10, FINSEQ_1:def 13;
then reconsider SA =
Sgm (F " ((Carrier L) /\ A)),
SB =
Sgm (F " ((Carrier L) /\ B)) as
FinSequence of
D by A16, A14, A15, FINSEQ_1:def 4;
A misses B
then A20:
(Carrier L) /\ A misses (Carrier L) /\ B
by XBOOLE_1:76;
then
F " ((Carrier L) /\ A) misses F " ((Carrier L) /\ B)
by FUNCT_1:71;
then A21:
(Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) is
one-to-one
by A11, A17, A13, A15, FINSEQ_3:91;
((Carrier L) /\ A) \/ ((Carrier L) /\ B) =
(Carrier L) /\ (A \/ B)
by XBOOLE_1:23
.=
Carrier L
by A1, XBOOLE_1:28
;
then A22:
(F " ((Carrier L) /\ A)) \/ (F " ((Carrier L) /\ B)) =
F " (Carrier L)
by RELAT_1:140
.=
dom F
by A4, RELAT_1:134
;
then (card (F " ((Carrier L) /\ A))) + (card (F " ((Carrier L) /\ B))) =
card (Seg (len F))
by A10, A20, CARD_2:40, FUNCT_1:71
.=
len F
by FINSEQ_1:57
;
then
len ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = len F
by A12, FINSEQ_1:22;
then A23:
dom ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D
by FINSEQ_3:29;
rng ((Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A)))) = D
by A22, A17, A15, FINSEQ_1:31;
then reconsider SS =
(Sgm (F " ((Carrier L) /\ B))) ^ (Sgm (F " ((Carrier L) /\ A))) as
Function of
D,
D by A23, FUNCT_2:1;
card D = card D
;
then
SS is
onto
by A21, FINSEQ_4:63;
then reconsider SS =
SS as
Permutation of
D by A21;
reconsider FS =
F9 * SS,
FSA =
F9 * SA,
FSB =
F9 * SB as
FinSequence of
V1 by FINSEQ_2:47;
A24:
(Carrier L) /\ B c= rng FSB
rng FSB c= (Carrier L) /\ B
then A31:
(Carrier L) /\ B = rng FSB
by A24;
A32:
now for k being Nat
for v being Element of V2 st k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k holds
(f * (L (#) FSA)) . k = (0. K) * v
len (L (#) FSA) = len FSA
by VECTSP_6:def 5;
then A33:
dom (L (#) FSA) = dom FSA
by FINSEQ_3:29;
A34:
dom f = [#] V1
by FUNCT_2:def 1;
(
rng (L (#) FSA) c= [#] V1 &
dom f = [#] V1 )
by FUNCT_2:def 1, RELAT_1:def 19;
then A35:
dom (f * (L (#) FSA)) = dom (L (#) FSA)
by RELAT_1:27;
let k be
Nat;
for v being Element of V2 st k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k holds
(f * (L (#) FSA)) . k = (0. K) * vlet v be
Element of
V2;
( k in dom (f * (L (#) FSA)) & v = (f * (L (#) FSA)) . k implies (f * (L (#) FSA)) . k = (0. K) * v )assume that A36:
k in dom (f * (L (#) FSA))
and
v = (f * (L (#) FSA)) . k
;
(f * (L (#) FSA)) . k = (0. K) * v
dom FSA = dom SA
by A17, RELAT_1:27, RELAT_1:132;
then
SA . k in F " ((Carrier L) /\ A)
by A17, A36, A35, A33, FUNCT_1:def 3;
then A37:
F . (SA . k) in (Carrier L) /\ A
by FUNCT_1:def 7;
FSA /. k =
FSA . k
by A36, A35, A33, PARTFUN1:def 6
.=
F . (SA . k)
by A36, A35, A33, FUNCT_1:12
;
then
FSA /. k in A
by A37, XBOOLE_0:def 4;
then
f . (FSA /. k) in f .: A
by A34, FUNCT_1:def 6;
then A38:
f . (FSA /. k) = 0. V2
by A8, TARSKI:def 1;
thus (f * (L (#) FSA)) . k =
f . ((L (#) FSA) . k)
by A36, FUNCT_1:12
.=
f . ((L . (FSA /. k)) * (FSA /. k))
by A36, A35, VECTSP_6:def 5
.=
(L . (FSA /. k)) * (0. V2)
by A38, MOD_2:def 2
.=
0. V2
by VECTSP_1:14
.=
(0. K) * v
by VECTSP_1:14
;
verum end;
len (f * (L (#) FSA)) = len (f * (L (#) FSA))
;
then A39:
Sum (f * (L (#) FSA)) = (0. K) * (Sum (f * (L (#) FSA)))
by A32, RLVECT_2:66;
FS = FSB ^ FSA
by FINSEQOP:9;
then
L (#) FS = (L (#) FSB) ^ (L (#) FSA)
by VECTSP_6:13;
then A40:
f * (L (#) FS) = (f * (L (#) FSB)) ^ (f * (L (#) FSA))
by FINSEQOP:9;
(f | B) | ((Carrier L) /\ B) = f | ((Carrier L) /\ B)
by RELAT_1:74, XBOOLE_1:18;
then A41:
f | ((Carrier L) /\ B) is
one-to-one
by A6, FUNCT_1:52;
then consider Lf being
Linear_Combination of
V2 such that A42:
Carrier Lf = f .: ((Carrier L) /\ (rng FSB))
and A43:
f * (L (#) FSB) = Lf (#) (f * FSB)
and A44:
for
v1 being
Vector of
V1 st
v1 in (Carrier L) /\ (rng FSB) holds
L . v1 = Lf . (f . v1)
by A31, A9, Th43, XBOOLE_1:18;
A45:
Carrier Lf = rng (f * FSB)
by A31, A9, A42, RELAT_1:127;
A46:
f * FSB =
f * ((id (rng FSB)) * FSB)
by RELAT_1:53
.=
(f * (id (rng FSB))) * FSB
by RELAT_1:36
.=
(f | ((Carrier L) /\ B)) * FSB
by A31, RELAT_1:65
;
Carrier Lf c= f .: B
by A31, A9, A42, RELAT_1:123, XBOOLE_1:18;
then A47:
Lf is
Linear_Combination of
f .: B
by VECTSP_6:def 4;
f . (0. V1) = 0. V2
by RANKNULL:9;
then A48:
0. V2 =
f . (Sum (L (#) FS))
by A5, VECTSP_9:1
.=
Sum (f * (L (#) FS))
by MATRLIN:16
.=
(Sum (f * (L (#) FSB))) + (Sum (f * (L (#) FSA)))
by A40, RLVECT_1:41
.=
(Sum (f * (L (#) FSB))) + (0. V2)
by A39, VECTSP_1:14
.=
Sum (Lf (#) (f * FSB))
by A43, RLVECT_1:def 4
.=
Sum Lf
by A3, A13, A41, A45, A46, VECTSP_6:def 6
;
thus
Carrier L c= A
verumproof
let x be
object ;
TARSKI:def 3 ( not x in Carrier L or x in A )
assume A49:
x in Carrier L
;
x in A
reconsider v1 =
x as
Vector of
V1 by A49;
assume A50:
not
x in A
;
contradiction
(
x in A or
x in B )
by A1, A49, XBOOLE_0:def 3;
then
v1 in (Carrier L) /\ (rng FSB)
by A31, A9, A49, A50, XBOOLE_0:def 4;
then A51:
L . v1 = Lf . (f . v1)
by A44;
not
f . v1 in Carrier Lf
by A7, A47, A48, VECTSP_7:def 1;
then
L . v1 = 0. K
by A51;
hence
contradiction
by A49, VECTSP_6:2;
verum
end; end; end;