let n be Nat; for F being one-to-one FinSequence of (TOP-REAL n) st rng F is linearly-independent holds
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let F be one-to-one FinSequence of (TOP-REAL n); ( rng F is linearly-independent implies for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A1:
rng F is linearly-independent
; for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
reconsider f = F as FinSequence of (n -VectSp_over F_Real) by Lm1;
set MF = FinS2MX f;
set n1 = n -' (len F);
set L = len F;
lines (FinS2MX f) is linearly-independent
by A1, Th7;
then
the_rank_of (FinS2MX f) = len F
by MATRIX13:121;
then
len F <= width (FinS2MX f)
by MATRIX13:74;
then A2:
len F <= n
by MATRIX_0:23;
then A3:
n - (len F) = n -' (len F)
by XREAL_1:233;
set V = n -VectSp_over F_Real;
let B be OrdBasis of n -VectSp_over F_Real; ( B = MX2FinS (1. (F_Real,n)) implies for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A4:
B = MX2FinS (1. (F_Real,n))
; for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let M be Matrix of n,F_Real; ( M is invertible & M | (len F) = F implies (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume that
M is invertible
and
A5:
M | (len F) = F
; (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
consider q being FinSequence such that
A6:
M = F ^ q
by A5, FINSEQ_1:80;
M = MX2FinS M
;
then reconsider q = q as FinSequence of (n -VectSp_over F_Real) by A6, FINSEQ_1:36;
A7:
len M = (len F) + (len q)
by A6, FINSEQ_1:22;
set Mq = FinS2MX q;
set MT = Mx2Tran M;
A8:
len M = n
by MATRIX_0:def 2;
A9:
dom (Mx2Tran M) = [#] (TOP-REAL n)
by FUNCT_2:52;
A10:
dom (Mx2Tran (FinS2MX f)) = [#] (TOP-REAL (len F))
by FUNCT_2:def 1;
A11: the carrier of (TOP-REAL n) =
REAL n
by EUCLID:22
.=
n -tuples_on REAL
;
A12: rng (Mx2Tran (FinS2MX f)) =
[#] (Lin (lines (FinS2MX f)))
by Th18
.=
[#] (Lin (rng F))
by Th6
;
A13: n |-> 0 =
0* n
.=
0. (TOP-REAL n)
by EUCLID:70
;
A14: (n -' (len F)) |-> 0 =
0* (n -' (len F))
.=
0. (TOP-REAL (n -' (len F)))
by EUCLID:70
;
then A15:
(Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0) = 0. (TOP-REAL n)
by A3, A8, A7, MATRTOP1:29;
thus
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) c= [#] (Lin (rng F))
XBOOLE_0:def 10 [#] (Lin (rng F)) c= (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))proof
let y be
object ;
TARSKI:def 3 ( not y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) or y in [#] (Lin (rng F)) )
assume
y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))
;
y in [#] (Lin (rng F))
then consider x being
object such that A16:
x in dom (Mx2Tran M)
and A17:
x in [#] (Lin (rng (B | (len F))))
and A18:
(Mx2Tran M) . x = y
by FUNCT_1:def 6;
reconsider x =
x as
Element of
(TOP-REAL n) by A16;
len x = n
by CARD_1:def 7;
then
len (x | (len F)) = len F
by A2, FINSEQ_1:59;
then A19:
x | (len F) is
len F -element
by CARD_1:def 7;
then A20:
x | (len F) is
Element of
(TOP-REAL (len F))
by Lm3;
A21:
(Mx2Tran (FinS2MX f)) . (x | (len F)) is
Element of
n -tuples_on REAL
by A11, A19, Lm3;
x in Lin (rng (B | (len F)))
by A17;
then
x = (x | (len F)) ^ ((n -' (len F)) |-> 0)
by A4, Th20;
then y =
((Mx2Tran (FinS2MX f)) . (x | (len F))) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0))
by A3, A8, A6, A7, A18, A19, MATRTOP1:36
.=
(Mx2Tran (FinS2MX f)) . (x | (len F))
by A13, A15, A21, RVSUM_1:16
;
hence
y in [#] (Lin (rng F))
by A12, A10, A20, FUNCT_1:def 3;
verum
end;
let y be object ; TARSKI:def 3 ( not y in [#] (Lin (rng F)) or y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) )
assume
y in [#] (Lin (rng F))
; y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))
then consider x being object such that
A22:
x in dom (Mx2Tran (FinS2MX f))
and
A23:
(Mx2Tran (FinS2MX f)) . x = y
by A12, FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL (len F)) by A22;
(Mx2Tran (FinS2MX f)) . x is Element of (TOP-REAL n)
by Lm3;
then A24: y =
((Mx2Tran (FinS2MX f)) . x) + (0. (TOP-REAL n))
by A11, A13, A23, RVSUM_1:16
.=
((Mx2Tran (FinS2MX f)) . x) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0))
by A3, A8, A7, A14, MATRTOP1:29
.=
(Mx2Tran M) . (x ^ ((n -' (len F)) |-> 0))
by A6, A3, A8, A7, MATRTOP1:36
;
set xx = x ^ ((n -' (len F)) |-> 0);
len x = len F
by CARD_1:def 7;
then
dom x = Seg (len F)
by FINSEQ_1:def 3;
then
x ^ ((n -' (len F)) |-> 0) = ((x ^ ((n -' (len F)) |-> 0)) | (len F)) ^ ((n -' (len F)) |-> 0)
by FINSEQ_1:21;
then
x ^ ((n -' (len F)) |-> 0) in Lin (rng (B | (len F)))
by A4, A3, Th20;
then A25:
x ^ ((n -' (len F)) |-> 0) in [#] (Lin (rng (B | (len F))))
;
x ^ ((n -' (len F)) |-> 0) is Element of (TOP-REAL n)
by A3, Lm3;
hence
y in (Mx2Tran M) .: ([#] (Lin (rng (B | (len F)))))
by A9, A24, A25, FUNCT_1:def 6; verum