Metamath Proof Explorer


Theorem pmtridfv1

Description: Value at X 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 φ A V
pmtridf1o.x φ X A
pmtridf1o.y φ Y A
pmtridf1o.t T = if X = Y I A pmTrsp A X Y
Assertion pmtridfv1 φ T X = Y

Proof

Step Hyp Ref Expression
1 pmtridf1o.a φ A V
2 pmtridf1o.x φ X A
3 pmtridf1o.y φ Y A
4 pmtridf1o.t T = if X = Y I A pmTrsp A X Y
5 simpr φ X = Y X = Y
6 5 iftrued φ X = Y if X = Y I A pmTrsp A X Y = I A
7 4 6 syl5eq φ X = Y T = I A
8 7 fveq1d φ X = Y T X = I A X
9 fvresi X A I A X = X
10 2 9 syl φ I A X = X
11 10 adantr φ X = Y I A X = X
12 8 11 5 3eqtrd φ X = Y T X = Y
13 simpr φ X Y X Y
14 13 neneqd φ X Y ¬ X = Y
15 14 iffalsed φ X Y if X = Y I A pmTrsp A X Y = pmTrsp A X Y
16 4 15 syl5eq φ X Y T = pmTrsp A X Y
17 16 fveq1d φ X Y T X = pmTrsp A X Y X
18 1 adantr φ X Y A V
19 2 adantr φ X Y X A
20 3 adantr φ X Y Y A
21 eqid pmTrsp A = pmTrsp A
22 21 pmtrprfv A V X A Y A X Y pmTrsp A X Y X = Y
23 18 19 20 13 22 syl13anc φ X Y pmTrsp A X Y X = Y
24 17 23 eqtrd φ X Y T X = Y
25 12 24 pm2.61dane φ T X = Y