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 = ( pmTrsp ` D )
pmtrrn.r
|- R = ran T
pmtrfrn.p
|- P = dom ( F \ _I )
Assertion pmtrffv
|- ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r
 |-  R = ran T
3 pmtrfrn.p
 |-  P = dom ( F \ _I )
4 1 2 3 pmtrfrn
 |-  ( F e. R -> ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ F = ( T ` P ) ) )
5 4 simprd
 |-  ( F e. R -> F = ( T ` P ) )
6 5 fveq1d
 |-  ( F e. R -> ( F ` Z ) = ( ( T ` P ) ` Z ) )
7 6 adantr
 |-  ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = ( ( T ` P ) ` Z ) )
8 4 simpld
 |-  ( F e. R -> ( D e. _V /\ P C_ D /\ P ~~ 2o ) )
9 1 pmtrfv
 |-  ( ( ( D e. _V /\ P C_ D /\ P ~~ 2o ) /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
10 8 9 sylan
 |-  ( ( F e. R /\ Z e. D ) -> ( ( T ` P ) ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )
11 7 10 eqtrd
 |-  ( ( F e. R /\ Z e. D ) -> ( F ` Z ) = if ( Z e. P , U. ( P \ { Z } ) , Z ) )