This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> A e. V )
pmtridf1o.x 
|- ( ph -> X e. A )
pmtridf1o.y 
|- ( ph -> Y e. A )
pmtridf1o.t 
|- T = if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) )
Assertion pmtridfv2 
|- ( ph -> ( T ` Y ) = X )

Proof

Step Hyp Ref Expression
1 pmtridf1o.a 
 |-  ( ph -> A e. V )
2 pmtridf1o.x 
 |-  ( ph -> X e. A )
3 pmtridf1o.y 
 |-  ( ph -> Y e. A )
4 pmtridf1o.t 
 |-  T = if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) )
5 fvresi 
 |-  ( Y e. A -> ( ( _I |` A ) ` Y ) = Y )
6 3 5 syl 
 |-  ( ph -> ( ( _I |` A ) ` Y ) = Y )
7 6 adantr 
 |-  ( ( ph /\ X = Y ) -> ( ( _I |` A ) ` Y ) = Y )
8 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
9 8 iftrued 
 |-  ( ( ph /\ X = Y ) -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( _I |` A ) )
10 4 9 eqtrid 
 |-  ( ( ph /\ X = Y ) -> T = ( _I |` A ) )
11 10 fveq1d 
 |-  ( ( ph /\ X = Y ) -> ( T ` Y ) = ( ( _I |` A ) ` Y ) )
12 7 11 8 3eqtr4d 
 |-  ( ( ph /\ X = Y ) -> ( T ` Y ) = X )
13 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
14 13 neneqd 
 |-  ( ( ph /\ X =/= Y ) -> -. X = Y )
15 14 iffalsed 
 |-  ( ( ph /\ X =/= Y ) -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( ( pmTrsp ` A ) ` { X , Y } ) )
16 4 15 eqtrid 
 |-  ( ( ph /\ X =/= Y ) -> T = ( ( pmTrsp ` A ) ` { X , Y } ) )
17 16 fveq1d 
 |-  ( ( ph /\ X =/= Y ) -> ( T ` Y ) = ( ( ( pmTrsp ` A ) ` { X , Y } ) ` Y ) )
18 1 adantr 
 |-  ( ( ph /\ X =/= Y ) -> A e. V )
19 2 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. A )
20 3 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. A )
21 eqid 
 |-  ( pmTrsp ` A ) = ( pmTrsp ` A )
22 21 pmtrprfv2 
 |-  ( ( A e. V /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( ( ( pmTrsp ` A ) ` { X , Y } ) ` Y ) = X )
23 18 19 20 13 22 syl13anc 
 |-  ( ( ph /\ X =/= Y ) -> ( ( ( pmTrsp ` A ) ` { X , Y } ) ` Y ) = X )
24 17 23 eqtrd 
 |-  ( ( ph /\ X =/= Y ) -> ( T ` Y ) = X )
25 12 24 pm2.61dane 
 |-  ( ph -> ( T ` Y ) = X )