Theorem pmtrffv

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

	Ref	Expression
Hypotheses	pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
	pmtrrn.r	⊢ 𝑅 = ran 𝑇
	pmtrfrn.p	⊢ 𝑃 = dom ( 𝐹 ∖ I )
Assertion	pmtrffv	⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		pmtrrn.t	⊢ 𝑇 = ( pmTrsp ‘ 𝐷 )
2		pmtrrn.r	⊢ 𝑅 = ran 𝑇
3		pmtrfrn.p	⊢ 𝑃 = dom ( 𝐹 ∖ I )
4	1 2 3	pmtrfrn	⊢ ( 𝐹 ∈ 𝑅 → ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝐹 = ( 𝑇 ‘ 𝑃 ) ) )
5	4	simprd	⊢ ( 𝐹 ∈ 𝑅 → 𝐹 = ( 𝑇 ‘ 𝑃 ) )
6	5	fveq1d	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐹 ‘ 𝑍 ) = ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) )
7	6	adantr	⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑍 ) = ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) )
8	4	simpld	⊢ ( 𝐹 ∈ 𝑅 → ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) )
9	1	pmtrfv	⊢ ( ( ( 𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o ) ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
10	8 9	sylan	⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷 ) → ( ( 𝑇 ‘ 𝑃 ) ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )
11	7 10	eqtrd	⊢ ( ( 𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑍 ) = if ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )