invisoinvl

Description: The inverse of an isomorphism F (which is unique because of invf and is therefore denoted by ( ( X N Y )F ) , see also remark 3.12 in Adamek p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020)

	Ref	Expression
Hypotheses	invisoinv.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invisoinv.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	invisoinv.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invisoinv.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invisoinv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invisoinv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	invisoinv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion	invisoinvl	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		invisoinv.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		invisoinv.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
3		invisoinv.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
4		invisoinv.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		invisoinv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		invisoinv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		invisoinv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
10	1 9 4 6	idiso	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( 𝑌 ( Iso ‘ 𝐶 ) 𝑌 ) )
11	2	a1i	⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐶 ) )
12	11	oveqd	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑌 ) = ( 𝑌 ( Iso ‘ 𝐶 ) 𝑌 ) )
13	10 12	eleqtrrd	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ∈ ( 𝑌 𝐼 𝑌 ) )
14	1 3 4 5 6 2 7 8 6 13	invco	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) ( 𝑋 𝑁 𝑌 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
15		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
16	1 15 2 4 5 6	isohom	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
17	16 7	sseldd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18	1 15 9 4 5 8 6 17	catlid	⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = 𝐹 )
19	3	a1i	⊢ ( 𝜑 → 𝑁 = ( Inv ‘ 𝐶 ) )
20	19	oveqd	⊢ ( 𝜑 → ( 𝑌 𝑁 𝑌 ) = ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) )
21	20	fveq1d	⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
22	1 9 4 6	idinv	⊢ ( 𝜑 → ( ( 𝑌 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
23	21 22	eqtrd	⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
24	23	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) = ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
25	1 15 2 4 6 5	isohom	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
26	1 3 4 5 6 2	invf	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
27	26 7	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
28	25 27	sseldd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
29	1 15 9 4 6 8 5 28	catrid	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
30	24 29	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑌 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( 𝑌 𝑁 𝑌 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) = ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
31	14 18 30	3brtr3d	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
32	1 3 4 6 5	invsym	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
33	31 32	mpbird	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )

Metamath Proof Explorer

Theorem invisoinvl

Proof