let k be Nat; :: thesis: for M being Matrix of k,F_Real holds Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))
let M be Matrix of k,F_Real; :: thesis: Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k))
reconsider M2 = Mx2Tran M as Function of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k)) by Th32;
A1: RLSp2RVSp (TOP-REAL k) = ModuleStr(# the carrier of (TOP-REAL k), the addF of (TOP-REAL k), the ZeroF of (TOP-REAL k),(MultF_Real* (TOP-REAL k)) #) by DUALSP01:def 2;
for x, y being Element of (RLSp2RVSp (TOP-REAL k)) holds M2 . (x + y) = (M2 . x) + (M2 . y)
proof
let x, y be Element of (RLSp2RVSp (TOP-REAL k)); :: thesis: M2 . (x + y) = (M2 . x) + (M2 . y)
reconsider xr = x, yr = y as Element of (TOP-REAL k) by A1;
A2: x + y = xr + yr by A1;
M2 . (x + y) = ((Mx2Tran M) . xr) + ((Mx2Tran M) . yr) by A2, MATRTOP1:22
.= (M2 . x) + (M2 . y) by A1 ;
hence M2 . (x + y) = (M2 . x) + (M2 . y) ; :: thesis: verum
end;
then A3: M2 is additive ;
for a being Scalar of F_Real
for x being Vector of (RLSp2RVSp (TOP-REAL k)) holds M2 . (a * x) = a * (M2 . x)
proof
let a be Scalar of F_Real; :: thesis: for x being Vector of (RLSp2RVSp (TOP-REAL k)) holds M2 . (a * x) = a * (M2 . x)
let x be Vector of (RLSp2RVSp (TOP-REAL k)); :: thesis: M2 . (a * x) = a * (M2 . x)
reconsider ra = a as Real ;
reconsider rx = x as Element of (TOP-REAL k) by A1;
reconsider X = RLSp2RVSp (TOP-REAL 3) as ModuleStr over F_Real ;
A4: a * x = a * rx
proof
MultF_Real* (TOP-REAL k) = the Mult of (TOP-REAL k) by DUALSP01:def 1;
hence a * x = a * rx by A1, RLVECT_1:def 1; :: thesis: verum
end;
a * ((Mx2Tran M) . x) = a * (M2 . x)
proof
a * (M2 . x) = the Mult of (TOP-REAL k) . (a,((Mx2Tran M) . x)) by A1, DUALSP01:def 1
.= a * ((Mx2Tran M) . rx) by RLVECT_1:def 1 ;
hence a * ((Mx2Tran M) . x) = a * (M2 . x) ; :: thesis: verum
end;
hence M2 . (a * x) = a * (M2 . x) by A4, MATRTOP1:23; :: thesis: verum
end;
hence Mx2Tran M is linear-transformation of (RLSp2RVSp (TOP-REAL k)),(RLSp2RVSp (TOP-REAL k)) by A3, MOD_2:def 2; :: thesis: verum