Metamath Proof Explorer


Theorem pmtrprfv3

Description: In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019)

Ref Expression
Hypothesis pmtrfval.t 𝑇 = ( pmTrsp ‘ 𝐷 )
Assertion pmtrprfv3 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 pmtrfval.t 𝑇 = ( pmTrsp ‘ 𝐷 )
2 simp1 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝐷𝑉 )
3 simp1 ( ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) → 𝑋𝐷 )
4 3 3ad2ant2 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝑋𝐷 )
5 simp22 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝑌𝐷 )
6 4 5 prssd ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { 𝑋 , 𝑌 } ⊆ 𝐷 )
7 pr2nelem ( ( 𝑋𝐷𝑌𝐷𝑋𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
8 7 3expia ( ( 𝑋𝐷𝑌𝐷 ) → ( 𝑋𝑌 → { 𝑋 , 𝑌 } ≈ 2o ) )
9 8 3adant3 ( ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) → ( 𝑋𝑌 → { 𝑋 , 𝑌 } ≈ 2o ) )
10 9 com12 ( 𝑋𝑌 → ( ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) → { 𝑋 , 𝑌 } ≈ 2o ) )
11 10 3ad2ant1 ( ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) → ( ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) → { 𝑋 , 𝑌 } ≈ 2o ) )
12 11 impcom ( ( ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
13 12 3adant1 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → { 𝑋 , 𝑌 } ≈ 2o )
14 simp23 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝑍𝐷 )
15 1 pmtrfv ( ( ( 𝐷𝑉 ∧ { 𝑋 , 𝑌 } ⊆ 𝐷 ∧ { 𝑋 , 𝑌 } ≈ 2o ) ∧ 𝑍𝐷 ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) )
16 2 6 13 14 15 syl31anc ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) )
17 necom ( 𝑋𝑍𝑍𝑋 )
18 17 biimpi ( 𝑋𝑍𝑍𝑋 )
19 18 3ad2ant2 ( ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) → 𝑍𝑋 )
20 19 3ad2ant3 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝑍𝑋 )
21 necom ( 𝑌𝑍𝑍𝑌 )
22 21 biimpi ( 𝑌𝑍𝑍𝑌 )
23 22 3ad2ant3 ( ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) → 𝑍𝑌 )
24 23 3ad2ant3 ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → 𝑍𝑌 )
25 20 24 nelprd ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ¬ 𝑍 ∈ { 𝑋 , 𝑌 } )
26 25 iffalsed ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → if ( 𝑍 ∈ { 𝑋 , 𝑌 } , ( { 𝑋 , 𝑌 } ∖ { 𝑍 } ) , 𝑍 ) = 𝑍 )
27 16 26 eqtrd ( ( 𝐷𝑉 ∧ ( 𝑋𝐷𝑌𝐷𝑍𝐷 ) ∧ ( 𝑋𝑌𝑋𝑍𝑌𝑍 ) ) → ( ( 𝑇 ‘ { 𝑋 , 𝑌 } ) ‘ 𝑍 ) = 𝑍 )