This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )