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

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 
|- ( 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 pmtridfv1 
|- ( ph -> ( T ` X ) = Y )

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 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
6 5 iftrued 
 |-  ( ( ph /\ X = Y ) -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( _I |` A ) )
7 4 6 eqtrid 
 |-  ( ( ph /\ X = Y ) -> T = ( _I |` A ) )
8 7 fveq1d 
 |-  ( ( ph /\ X = Y ) -> ( T ` X ) = ( ( _I |` A ) ` X ) )
9 fvresi 
 |-  ( X e. A -> ( ( _I |` A ) ` X ) = X )
10 2 9 syl 
 |-  ( ph -> ( ( _I |` A ) ` X ) = X )
11 10 adantr 
 |-  ( ( ph /\ X = Y ) -> ( ( _I |` A ) ` X ) = X )
12 8 11 5 3eqtrd 
 |-  ( ( ph /\ X = Y ) -> ( T ` X ) = Y )
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 ` X ) = ( ( ( pmTrsp ` A ) ` { X , Y } ) ` X ) )
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 pmtrprfv 
 |-  ( ( A e. V /\ ( X e. A /\ Y e. A /\ X =/= Y ) ) -> ( ( ( pmTrsp ` A ) ` { X , Y } ) ` X ) = Y )
23 18 19 20 13 22 syl13anc 
 |-  ( ( ph /\ X =/= Y ) -> ( ( ( pmTrsp ` A ) ` { X , Y } ) ` X ) = Y )
24 17 23 eqtrd 
 |-  ( ( ph /\ X =/= Y ) -> ( T ` X ) = Y )
25 12 24 pm2.61dane 
 |-  ( ph -> ( T ` X ) = Y )