Metamath Proof Explorer


Theorem pmtridfv2

Description: Value at Y of the transposition of X and Y (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022)

Ref Expression
Hypotheses pmtridf1o.a ( 𝜑𝐴𝑉 )
pmtridf1o.x ( 𝜑𝑋𝐴 )
pmtridf1o.y ( 𝜑𝑌𝐴 )
pmtridf1o.t 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
Assertion pmtridfv2 ( 𝜑 → ( 𝑇𝑌 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 pmtridf1o.a ( 𝜑𝐴𝑉 )
2 pmtridf1o.x ( 𝜑𝑋𝐴 )
3 pmtridf1o.y ( 𝜑𝑌𝐴 )
4 pmtridf1o.t 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
5 fvresi ( 𝑌𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
6 3 5 syl ( 𝜑 → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
7 6 adantr ( ( 𝜑𝑋 = 𝑌 ) → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
8 simpr ( ( 𝜑𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
9 8 iftrued ( ( 𝜑𝑋 = 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( I ↾ 𝐴 ) )
10 4 9 syl5eq ( ( 𝜑𝑋 = 𝑌 ) → 𝑇 = ( I ↾ 𝐴 ) )
11 10 fveq1d ( ( 𝜑𝑋 = 𝑌 ) → ( 𝑇𝑌 ) = ( ( I ↾ 𝐴 ) ‘ 𝑌 ) )
12 7 11 8 3eqtr4d ( ( 𝜑𝑋 = 𝑌 ) → ( 𝑇𝑌 ) = 𝑋 )
13 simpr ( ( 𝜑𝑋𝑌 ) → 𝑋𝑌 )
14 13 neneqd ( ( 𝜑𝑋𝑌 ) → ¬ 𝑋 = 𝑌 )
15 14 iffalsed ( ( 𝜑𝑋𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
16 4 15 syl5eq ( ( 𝜑𝑋𝑌 ) → 𝑇 = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
17 16 fveq1d ( ( 𝜑𝑋𝑌 ) → ( 𝑇𝑌 ) = ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) )
18 1 adantr ( ( 𝜑𝑋𝑌 ) → 𝐴𝑉 )
19 2 adantr ( ( 𝜑𝑋𝑌 ) → 𝑋𝐴 )
20 3 adantr ( ( 𝜑𝑋𝑌 ) → 𝑌𝐴 )
21 eqid ( pmTrsp ‘ 𝐴 ) = ( pmTrsp ‘ 𝐴 )
22 21 pmtrprfv2 ( ( 𝐴𝑉 ∧ ( 𝑋𝐴𝑌𝐴𝑋𝑌 ) ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )
23 18 19 20 13 22 syl13anc ( ( 𝜑𝑋𝑌 ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )
24 17 23 eqtrd ( ( 𝜑𝑋𝑌 ) → ( 𝑇𝑌 ) = 𝑋 )
25 12 24 pm2.61dane ( 𝜑 → ( 𝑇𝑌 ) = 𝑋 )