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 ∈ R ∧ Z ∈ D → F ⁡ Z = if Z ∈ P ⋃ 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 ∈ R → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ F = T ⁡ P
5 4 simprd ⊢ F ∈ R → F = T ⁡ P
6 5 fveq1d ⊢ F ∈ R → F ⁡ Z = T ⁡ P ⁡ Z
7 6 adantr ⊢ F ∈ R ∧ Z ∈ D → F ⁡ Z = T ⁡ P ⁡ Z
8 4 simpld ⊢ F ∈ R → D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜
9 1 pmtrfv ⊢ D ∈ V ∧ P ⊆ D ∧ P ≈ 2 𝑜 ∧ Z ∈ D → T ⁡ P ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z
10 8 9 sylan ⊢ F ∈ R ∧ Z ∈ D → T ⁡ P ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z
11 7 10 eqtrd ⊢ F ∈ R ∧ Z ∈ D → F ⁡ Z = if Z ∈ P ⋃ P ∖ Z Z