let V be RealLinearSpace; for W being Subspace of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let W be Subspace of V; for L being Linear_Combination of V st Carrier L c= the carrier of W holds
for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let L be Linear_Combination of V; ( Carrier L c= the carrier of W implies for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K ) )
assume A1:
Carrier L c= the carrier of W
; for K being Linear_Combination of W st K = L | the carrier of W holds
( Carrier L = Carrier K & Sum L = Sum K )
let K be Linear_Combination of W; ( K = L | the carrier of W implies ( Carrier L = Carrier K & Sum L = Sum K ) )
assume A2:
K = L | the carrier of W
; ( Carrier L = Carrier K & Sum L = Sum K )
A3:
dom K = the carrier of W
by FUNCT_2:def 1;
then A7:
Carrier K c= Carrier L
;
consider G being FinSequence of the carrier of W such that
A8:
( G is one-to-one & rng G = Carrier K )
and
A9:
Sum K = Sum (K (#) G)
by RLVECT_2:def 8;
consider F being FinSequence of the carrier of V such that
A10:
F is one-to-one
and
A11:
rng F = Carrier L
and
A12:
Sum L = Sum (L (#) F)
by RLVECT_2:def 8;
then A16:
Carrier L c= Carrier K
;
then A17:
Carrier K = Carrier L
by A7, XBOOLE_0:def 10;
then
F,G are_fiberwise_equipotent
by A10, A11, A8, RFINSEQ:26;
then consider P being Permutation of (dom G) such that
A18:
F = G * P
by RFINSEQ:4;
len (K (#) G) = len G
by RLVECT_2:def 7;
then A19:
dom (K (#) G) = dom G
by FINSEQ_3:29;
then reconsider q = (K (#) G) * P as FinSequence of the carrier of W by FINSEQ_2:47;
A20:
len q = len (K (#) G)
by A19, FINSEQ_2:44;
then
len q = len G
by RLVECT_2:def 7;
then A21:
dom q = dom G
by FINSEQ_3:29;
set p = L (#) F;
A22:
the carrier of W c= the carrier of V
by RLSUB_1:def 2;
rng q c= the carrier of W
by FINSEQ_1:def 4;
then
rng q c= the carrier of V
by A22;
then reconsider q9 = q as FinSequence of the carrier of V by FINSEQ_1:def 4;
consider f being sequence of the carrier of W such that
A23:
Sum q = f . (len q)
and
A24:
f . 0 = 0. W
and
A25:
for i being Nat
for w being VECTOR of W st i < len q & w = q . (i + 1) holds
f . (i + 1) = (f . i) + w
by RLVECT_1:def 12;
( dom f = NAT & rng f c= the carrier of W )
by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f9 = f as sequence of the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1;
A26:
for i being Nat
for v being VECTOR of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v
A29:
len G = len F
by A18, FINSEQ_2:44;
then A30:
dom G = dom F
by FINSEQ_3:29;
len G = len (L (#) F)
by A29, RLVECT_2:def 7;
then A31:
dom (L (#) F) = dom G
by FINSEQ_3:29;
A32:
dom q = dom (K (#) G)
by A20, FINSEQ_3:29;
now for i being Nat st i in dom (L (#) F) holds
(L (#) F) . i = q . ilet i be
Nat;
( i in dom (L (#) F) implies (L (#) F) . i = q . i )set v =
F /. i;
set j =
P . i;
assume A33:
i in dom (L (#) F)
;
(L (#) F) . i = q . ithen A34:
F /. i = F . i
by A31, A30, PARTFUN1:def 6;
then
F /. i in rng F
by A31, A30, A33, FUNCT_1:def 3;
then reconsider w =
F /. i as
VECTOR of
W by A17, A11;
(
dom P = dom G &
rng P = dom G )
by FUNCT_2:52, FUNCT_2:def 3;
then A35:
P . i in dom G
by A31, A33, FUNCT_1:def 3;
then reconsider j =
P . i as
Element of
NAT ;
A36:
G /. j =
G . (P . i)
by A35, PARTFUN1:def 6
.=
F /. i
by A18, A31, A30, A33, A34, FUNCT_1:12
;
q . i =
(K (#) G) . j
by A31, A21, A33, FUNCT_1:12
.=
(K . w) * w
by A32, A21, A35, A36, RLVECT_2:def 7
.=
(L . (F /. i)) * w
by A2, A3, FUNCT_1:47
.=
(L . (F /. i)) * (F /. i)
by RLSUB_1:14
;
hence
(L (#) F) . i = q . i
by A33, RLVECT_2:def 7;
verum end;
then A37:
L (#) F = (K (#) G) * P
by A31, A21, FINSEQ_1:13;
len G = len (K (#) G)
by RLVECT_2:def 7;
then
dom G = dom (K (#) G)
by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom (K (#) G)) ;
q = (K (#) G) * P
;
then A38:
Sum (K (#) G) = Sum q
by RLVECT_2:7;
A39:
f9 . (len q9) is Element of V
;
f9 . 0 = 0. V
by A24, RLSUB_1:11;
hence
( Carrier L = Carrier K & Sum L = Sum K )
by A7, A16, A12, A9, A37, A38, A23, A26, A39, RLVECT_1:def 12, XBOOLE_0:def 10; verum