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