let n, m be Nat; for f being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let f be n -element real-valued FinSequence; for M being Matrix of n,m,F_Real
for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let M be Matrix of n,m,F_Real; for P being Permutation of (Seg n) holds
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
let P be Permutation of (Seg n); ( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
A1:
len f = n
by CARD_1:def 7;
then A2:
( rng P = Seg n & dom f = Seg n )
by FINSEQ_1:def 3, FUNCT_2:def 3;
dom P = Seg n
by FUNCT_2:52;
then A3:
dom (f * P) = Seg n
by A2, RELAT_1:27;
then reconsider fP = f * P as FinSequence by FINSEQ_1:def 2;
rng (f * P) = rng f
by A2, RELAT_1:28;
then reconsider fP = fP as FinSequence of REAL by FINSEQ_1:def 4;
A4:
len fP = n
by A1, A3, FINSEQ_1:def 3;
then A5:
fP is n -element
by CARD_1:def 7;
(Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)
proof
per cases
( n <> 0 or n = 0 )
;
suppose A6:
n <> 0
;
(Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)then A7:
width M = m
by MATRIX13:1;
set MP =
M * P;
A8:
len M = n
by A6, MATRIX13:1;
A9:
now for i being Nat st 1 <= i & i <= m holds
((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . ilet i be
Nat;
( 1 <= i & i <= m implies ((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . i )assume A10:
( 1
<= i &
i <= m )
;
((Mx2Tran (M * P)) . fP) . i = ((Mx2Tran M) . f) . ithen
i in Seg m
;
then A11:
mlt (
(@ fP),
(Col ((M * P),i))) =
the
multF of
F_Real .: (
fP,
((Col (M,i)) * P))
by A7, Th15
.=
(mlt ((@ f),(Col (M,i)))) * P
by FUNCOP_1:25
;
len (Col (M,i)) = n
by A8, CARD_1:def 7;
then
len (mlt ((@ f),(Col (M,i)))) = n
by A1, MATRIX_3:6;
then A12:
dom (mlt ((@ f),(Col (M,i)))) = Seg n
by FINSEQ_1:def 3;
((Mx2Tran (M * P)) . fP) . i =
(@ fP) "*" (Col ((M * P),i))
by A6, A5, A10, Th18
.=
the
addF of
F_Real "**" (mlt ((@ fP),(Col ((M * P),i))))
;
hence ((Mx2Tran (M * P)) . fP) . i =
(@ f) "*" (Col (M,i))
by A12, A11, FINSOP_1:7
.=
((Mx2Tran M) . f) . i
by A6, A10, Th18
;
verum end;
(
len ((Mx2Tran M) . f) = m &
len ((Mx2Tran (M * P)) . fP) = m )
by A5, CARD_1:def 7;
hence
(Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P)
by A9;
verum end; end;
end;
hence
( (Mx2Tran M) . f = (Mx2Tran (M * P)) . (f * P) & f * P is n -element FinSequence of REAL )
by A4, CARD_1:def 7; verum