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_1: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 A5:
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
A7:
M | (len F) = F
; (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
consider q being FinSequence such that
A8:
M = F ^ q
by A7, FINSEQ_1:80;
M = MX2FinS M
;
then reconsider q = q as FinSequence of (n -VectSp_over F_Real) by A8, FINSEQ_1:36;
A9:
len M = (len F) + (len q)
by A8, FINSEQ_1:22;
set Mq = FinS2MX q;
set MT = Mx2Tran M;
A11:
len M = n
by MATRIX_1:def 2;
A12:
dom (Mx2Tran M) = [#] (TOP-REAL n)
by FUNCT_2:52;
A21:
dom (Mx2Tran (FinS2MX f)) = [#] (TOP-REAL (len F))
by FUNCT_2:def 1;
A22: the carrier of (TOP-REAL n) =
REAL n
by EUCLID:22
.=
n -tuples_on REAL
;
A23: rng (Mx2Tran (FinS2MX f)) =
[#] (Lin (lines (FinS2MX f)))
by Th18
.=
[#] (Lin (rng F))
by Th6
;
A24: n |-> 0 =
0* n
.=
0. (TOP-REAL n)
by EUCLID:70
;
A25: (n -' (len F)) |-> 0 =
0* (n -' (len F))
.=
0. (TOP-REAL (n -' (len F)))
by EUCLID:70
;
then A26:
(Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0) = 0. (TOP-REAL n)
by A3, A11, A9, 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
set ;
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
set such that A27:
x in dom (Mx2Tran M)
and A28:
x in [#] (Lin (rng (B | (len F))))
and A29:
(Mx2Tran M) . x = y
by FUNCT_1:def 6;
reconsider x =
x as
Element of
(TOP-REAL n) by A27;
len x = n
by CARD_1:def 7;
then
len (x | (len F)) = len F
by A2, FINSEQ_1:59;
then A30:
x | (len F) is
len F -element
by CARD_1:def 7;
then A31:
x | (len F) is
Element of
(TOP-REAL (len F))
by Lm3;
A32:
(Mx2Tran (FinS2MX f)) . (x | (len F)) is
Element of
n -tuples_on REAL
by A22, A30, Lm3;
x in Lin (rng (B | (len F)))
by A28, STRUCT_0:def 5;
then
x = (x | (len F)) ^ ((n -' (len F)) |-> 0)
by A5, Th20;
then y =
((Mx2Tran (FinS2MX f)) . (x | (len F))) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0))
by A3, A11, A8, A9, A29, A30, MATRTOP1:36
.=
(Mx2Tran (FinS2MX f)) . (x | (len F))
by A24, A26, A32, RVSUM_1:16
;
hence
y in [#] (Lin (rng F))
by A23, A21, A31, FUNCT_1:def 3;
verum
end;
let y be set ; 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 set such that
A33:
x in dom (Mx2Tran (FinS2MX f))
and
A34:
(Mx2Tran (FinS2MX f)) . x = y
by A23, FUNCT_1:def 3;
reconsider x = x as Element of (TOP-REAL (len F)) by A33;
(Mx2Tran (FinS2MX f)) . x is Element of (TOP-REAL n)
by Lm3;
then A35: y =
((Mx2Tran (FinS2MX f)) . x) + (0. (TOP-REAL n))
by A22, A24, A34, RVSUM_1:16
.=
((Mx2Tran (FinS2MX f)) . x) + ((Mx2Tran (FinS2MX q)) . ((n -' (len F)) |-> 0))
by A3, A11, A9, A25, MATRTOP1:29
.=
(Mx2Tran M) . (x ^ ((n -' (len F)) |-> 0))
by A8, A3, A11, A9, 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 A5, A3, Th20;
then A36:
x ^ ((n -' (len F)) |-> 0) in [#] (Lin (rng (B | (len F))))
by STRUCT_0:def 5;
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 A12, A35, A36, FUNCT_1:def 6; verum