let n be Nat; :: thesis: for A, B being linearly-independent Subset of (TOP-REAL n) st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
set TRn = TOP-REAL n;
let A, B be linearly-independent Subset of (TOP-REAL n); :: thesis: ( card A = card B implies ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) ) )
assume A1: card A = card B ; :: thesis: ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
reconsider BB = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
set V = n -VectSp_over F_Real;
A is linearly-independent Subset of (n -VectSp_over F_Real) by Lm1, Th7;
then A is finite by VECTSP_9:21;
then consider fA being FinSequence such that
A2: rng fA = A and
A3: fA is one-to-one by FINSEQ_4:58;
A4: len fA = card A by A2, A3, PRE_POLY:19;
B is linearly-independent Subset of (n -VectSp_over F_Real) by Lm1, Th7;
then B is finite by VECTSP_9:21;
then consider fB being FinSequence such that
A5: rng fB = B and
A6: fB is one-to-one by FINSEQ_4:58;
A7: len fB = card B by A5, A6, PRE_POLY:19;
reconsider fA = fA, fB = fB as FinSequence of (TOP-REAL n) by A2, A5, FINSEQ_1:def 4;
consider MA being Matrix of n,F_Real such that
A8: MA is invertible and
A9: MA | (len fA) = fA by A2, A3, Th19;
A10: [#] (Lin (rng (BB | (len fA)))) c= [#] (n -VectSp_over F_Real) by VECTSP_4:def 2;
set Ma = Mx2Tran MA;
A11: Det MA <> 0. F_Real by A8, LAPLACE:34;
then A12: Mx2Tran MA is one-to-one by MATRTOP1:40;
then A13: rng ((Mx2Tran MA) ") = dom (Mx2Tran MA) by FUNCT_1:33;
A14: ( [#] (TOP-REAL n) = [#] (n -VectSp_over F_Real) & dom (Mx2Tran MA) = [#] (TOP-REAL n) ) by Lm1, FUNCT_2:52;
((Mx2Tran MA) ") " ([#] (Lin (rng (BB | (len fA))))) = (Mx2Tran MA) .: ([#] (Lin (rng (BB | (len fA))))) by A12, FUNCT_1:84
.= [#] (Lin A) by A2, A3, A8, A9, Th21 ;
then A15: ((Mx2Tran MA) ") .: ([#] (Lin A)) = [#] (Lin (rng (BB | (len fB)))) by A1, A4, A7, A14, A13, A10, FUNCT_1:77;
consider MB being Matrix of n,F_Real such that
A16: MB is invertible and
A17: MB | (len fB) = fB by A5, A6, Th19;
set Mb = Mx2Tran MB;
A18: ( n = 0 implies n = 0 ) ;
then width (MA ~) = n by MATRIX13:1;
then reconsider mb = MB as Matrix of width (MA ~),n,F_Real ;
A19: width MB = n by A18, MATRIX13:1;
reconsider MM = (MA ~) * mb as Matrix of n,F_Real ;
take MM ; :: thesis: ( MM is invertible & (Mx2Tran MM) .: ([#] (Lin A)) = [#] (Lin B) )
MA ~ is invertible by A8;
hence MM is invertible by A16, MATRIX_6:45; :: thesis: (Mx2Tran MM) .: ([#] (Lin A)) = [#] (Lin B)
(Mx2Tran MB) * ((Mx2Tran MA) ") = (Mx2Tran mb) * ((Mx2Tran MA) ") by A18, MATRIX13:1
.= (Mx2Tran mb) * (Mx2Tran (MA ~)) by A11, MATRTOP1:43
.= Mx2Tran ((MA ~) * mb) by A18, MATRTOP1:32
.= Mx2Tran MM by A18, A19, MATRIX13:1 ;
hence (Mx2Tran MM) .: ([#] (Lin A)) = (Mx2Tran MB) .: ([#] (Lin (rng (BB | (len fB))))) by A15, RELAT_1:126
.= [#] (Lin B) by A5, A6, A16, A17, Th21 ;
:: thesis: verum