isocoinvid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 10-Apr-2020)

	Ref	Expression
Hypotheses	invisoinv.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	invisoinv.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	invisoinv.n	⊢ 𝑁 = ( Inv ‘ 𝐶 )
	invisoinv.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	invisoinv.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	invisoinv.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	invisoinv.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
	invcoisoid.1	⊢ 1 = ( Id ‘ 𝐶 )
	isocoinvid.o	⊢ ⚬ = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
Assertion	isocoinvid	⊢ ( 𝜑 → ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) )

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		invcoisoid.1	⊢ 1 = ( Id ‘ 𝐶 )
9		isocoinvid.o	⊢ ⚬ = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 )
10	1 2 3 4 5 6 7	invisoinvl	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 )
11		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12	1 3 4 6 5 11	isinv	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 ↔ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) ) )
13		simpl	⊢ ( ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ∧ 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
14	12 13	syl6bi	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 𝑁 𝑋 ) 𝐹 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
15	10 14	mpd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
16		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
18	1 16 2 4 6 5	isohom	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
19	1 3 4 5 6 2	invf	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
20	19 7	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
21	18 20	sseldd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
22	1 16 2 4 5 6	isohom	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
23	22 7	sseldd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
24	1 16 17 8 11 4 6 5 21 23	issect2	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) ) )
25	9	a1i	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) )
26	25	eqcomd	⊢ ( 𝜑 → ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) = ⚬ )
27	26	oveqd	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
28	27	eqeq1d	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) ↔ ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) ) )
29	24 28	bitrd	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) ) )
30	15 29	mpbid	⊢ ( 𝜑 → ( 𝐹 ⚬ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) = ( 1 ‘ 𝑌 ) )

Metamath Proof Explorer

Theorem isocoinvid

Proof