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 syl5eq
 |-  ( ( 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 syl5eq
 |-  ( ( 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 )