Description: Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmtrrn.t | |
|
pmtrrn.r | |
||
pmtrfrn.p | |
||
Assertion | pmtrffv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmtrrn.t | |
|
2 | pmtrrn.r | |
|
3 | pmtrfrn.p | |
|
4 | 1 2 3 | pmtrfrn | |
5 | 4 | simprd | |
6 | 5 | fveq1d | |
7 | 6 | adantr | |
8 | 4 | simpld | |
9 | 1 | pmtrfv | |
10 | 8 9 | sylan | |
11 | 7 10 | eqtrd | |