let n, m be Nat; for M being Matrix of n,m,F_Real
for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let M be Matrix of n,m,F_Real; for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let Bn be OrdBasis of n -VectSp_over F_Real; for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
let Bm be OrdBasis of m -VectSp_over F_Real; ( Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) implies for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume that
A1:
Bn = MX2FinS (1. (F_Real,n))
and
A2:
Bm = MX2FinS (1. (F_Real,m))
; for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set T = Mx2Tran M;
let M1 be Matrix of len Bn, len Bm,F_Real; ( M1 = M implies Mx2Tran M = Mx2Tran (M1,Bn,Bm) )
assume A3:
M1 = M
; Mx2Tran M = Mx2Tran (M1,Bn,Bm)
set Tb = Mx2Tran (M1,Bn,Bm);
dom (Mx2Tran (M1,Bn,Bm)) = the carrier of (n -VectSp_over F_Real)
by FUNCT_2:def 1;
then A4: dom (Mx2Tran (M1,Bn,Bm)) =
REAL n
by MATRIX13:102
.=
the carrier of (TOP-REAL n)
by EUCLID:22
;
A5:
for x being object st x in dom (Mx2Tran M) holds
(Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
proof
let x be
object ;
( x in dom (Mx2Tran M) implies (Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x )
assume
x in dom (Mx2Tran M)
;
(Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . x
then reconsider v =
x as
Element of
(TOP-REAL n) by FUNCT_2:def 1;
reconsider g =
v as
Vector of
(n -VectSp_over F_Real) by A4, FUNCT_2:def 1;
set L =
LineVec2Mx (@ v);
len v = n
by CARD_1:def 7;
then A6:
(
len (LineVec2Mx (@ v)) = 1 &
width (LineVec2Mx (@ v)) = n )
by MATRIX13:1;
A7:
len Bn = n
by A1, Th19;
A8:
len Bm = m
by A2, Th19;
per cases
( n = 0 or n > 0 )
;
suppose A10:
n > 0
;
(Mx2Tran M) . x = (Mx2Tran (M1,Bn,Bm)) . xA11:
((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm = (Mx2Tran (M1,Bn,Bm)) . g
by A2, A8, MATRLIN2:46;
A12:
(
g |-- Bn = g &
AutMt (
(Mx2Tran (M1,Bn,Bm)),
Bn,
Bm)
= M )
by A1, A3, A7, MATRLIN2:36, MATRLIN2:46;
( 1
in dom (LineVec2Mx (@ v)) &
len M = width (LineVec2Mx (@ v)) )
by A10, A6, FINSEQ_3:25, MATRIX13:1;
then LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1)) =
(LineVec2Mx (Line ((LineVec2Mx (@ v)),1))) * M
by MATRLIN2:35
.=
(LineVec2Mx (@ v)) * M
by MATRIX15:25
.=
LineVec2Mx (((Mx2Tran (M1,Bn,Bm)) . g) |-- Bm)
by A7, A10, A12, MATRLIN2:31
;
hence (Mx2Tran (M1,Bn,Bm)) . x =
Line (
(LineVec2Mx (Line (((LineVec2Mx (@ v)) * M),1))),1)
by A11, MATRIX15:25
.=
Line (
((LineVec2Mx (@ v)) * M),1)
by MATRIX15:25
.=
(Mx2Tran M) . x
by A10, Def3
;
verum end;
end;
dom (Mx2Tran M) = the carrier of (TOP-REAL n)
by FUNCT_2:def 1;
hence
Mx2Tran M = Mx2Tran (M1,Bn,Bm)
by A4, A5, FUNCT_1:2; verum