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 )