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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	pmtridf1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	pmtridf1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	pmtridf1o.t	⊢ 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
Assertion	pmtridfv2	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑌 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		pmtridf1o.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		pmtridf1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		pmtridf1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
4		pmtridf1o.t	⊢ 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
5		fvresi	⊢ ( 𝑌 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
6	3 5	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( ( I ↾ 𝐴 ) ‘ 𝑌 ) = 𝑌 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
9	8	iftrued	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( I ↾ 𝐴 ) )
10	4 9	eqtrid	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑇 = ( I ↾ 𝐴 ) )
11	10	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑇 ‘ 𝑌 ) = ( ( I ↾ 𝐴 ) ‘ 𝑌 ) )
12	7 11 8	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑇 ‘ 𝑌 ) = 𝑋 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
14	13	neneqd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑋 = 𝑌 )
15	14	iffalsed	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
16	4 15	eqtrid	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑇 = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
17	16	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑇 ‘ 𝑌 ) = ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) )
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ 𝑉 )
19	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐴 )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐴 )
21		eqid	⊢ ( pmTrsp ‘ 𝐴 ) = ( pmTrsp ‘ 𝐴 )
22	21	pmtrprfv2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )
23	18 19 20 13 22	syl13anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑌 ) = 𝑋 )
24	17 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑇 ‘ 𝑌 ) = 𝑋 )
25	12 24	pm2.61dane	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑌 ) = 𝑋 )

Metamath Proof Explorer

Theorem pmtridfv2

Proof