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