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 ⊢ 𝑇 = ( 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 ( 𝑍 ∈ 𝑃 , ∪ ( 𝑃 ∖ { 𝑍 } ) , 𝑍 ) )