Metamath Proof Explorer

Theorem monsect

Description: If F is a monomorphism and G is a section of F , then G is an inverse of F and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses sectmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
sectmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
sectmon.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
sectmon.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
sectmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
sectmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
monsect.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
monsect.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
monsect.2 ⊢ ( 𝜑 → 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 )
Assertion monsect ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 sectmon.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 sectmon.m ⊢ 𝑀 = ( Mono ‘ 𝐶 )
3 sectmon.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
4 sectmon.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 sectmon.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 sectmon.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 monsect.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
8 monsect.1 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )
9 monsect.2 ⊢ ( 𝜑 → 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 )
10 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
11 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
12 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
13 1 10 11 12 3 4 6 5 issect ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ↔ ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
14 9 13 mpbid ⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
15 14 simp3d ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
16 15 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) )
17 14 simp2d ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
18 14 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
19 1 10 11 4 5 6 5 17 18 6 17 catass ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐺 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
20 1 10 12 4 5 11 6 17 catlid ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = 𝐹 )
21 1 10 12 4 5 11 6 17 catrid ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝐹 )
22 20 21 eqtr4d ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝐹 ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
23 16 19 22 3eqtr3d ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
24 1 10 11 4 5 6 5 17 18 catcocl ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
25 1 10 12 4 5 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
26 1 10 11 2 4 5 6 5 8 24 25 moni ⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) = ( 𝐹 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
27 23 26 mpbid ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
28 1 10 11 12 3 4 5 6 17 18 issect2 ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
29 27 28 mpbird ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
30 1 7 4 5 6 3 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 𝑆 𝑋 ) 𝐹 ) ) )
31 29 9 30 mpbir2and ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )