Metamath Proof Explorer


Theorem pmtrffv

Description: Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t T=pmTrspD
pmtrrn.r R=ranT
pmtrfrn.p P=domFI
Assertion pmtrffv FRZDFZ=ifZPPZZ

Proof

Step Hyp Ref Expression
1 pmtrrn.t T=pmTrspD
2 pmtrrn.r R=ranT
3 pmtrfrn.p P=domFI
4 1 2 3 pmtrfrn FRDVPDP2𝑜F=TP
5 4 simprd FRF=TP
6 5 fveq1d FRFZ=TPZ
7 6 adantr FRZDFZ=TPZ
8 4 simpld FRDVPDP2𝑜
9 1 pmtrfv DVPDP2𝑜ZDTPZ=ifZPPZZ
10 8 9 sylan FRZDTPZ=ifZPPZZ
11 7 10 eqtrd FRZDFZ=ifZPPZZ