invcoisoid

Description: The inverse of an isomorphism composed with the isomorphism is the identity. (Contributed by AV, 5-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 ‘ 𝐶 )
	invcoisoid.o	⊢ ⚬ = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
Assertion	invcoisoid	⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ⚬ 𝐹 ) = ( 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		invcoisoid.o	⊢ ⚬ = ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 )
10	1 2 3 4 5 6 7	invisoinvr	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
11		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12	1 3 4 5 6 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 5 6	isohom	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
19	18 7	sseldd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
20	1 16 2 4 6 5	isohom	⊢ ( 𝜑 → ( 𝑌 𝐼 𝑋 ) ⊆ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
21	1 3 4 5 6 2	invf	⊢ ( 𝜑 → ( 𝑋 𝑁 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
22	21 7	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
23	20 22	sseldd	⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
24	1 16 17 8 11 4 5 6 19 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 invcoisoid

Proof