Metamath Proof Explorer

Theorem sectmon

Description: If F is a section of G , then F is a monomorphism. A monomorphism that arises from a section is also known as asplit monomorphism. (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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
sectmon.1 ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
Assertion sectmon ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )

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 sectmon.1 ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 1 8 9 10 3 4 5 6 issect ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
12 7 11 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
13 12 simp1d ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
14 oveq2 ⊢ ( ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) = ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ) )
15 12 simp3d ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
16 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
17 16 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) )
18 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐶 ∈ Cat )
19 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑥 ∈ 𝐵 )
20 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
21 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑌 ∈ 𝐵 )
22 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) )
23 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
24 12 simp2d ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
26 1 8 9 18 19 20 21 22 23 20 25 catass ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) )
27 1 8 10 18 19 9 20 22 catlid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑔 ) = 𝑔 )
28 17 26 27 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) = 𝑔 )
29 16 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) = ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) )
30 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) )
31 1 8 9 18 19 20 21 30 23 20 25 catass ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) = ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ) )
32 1 8 10 18 19 9 20 30 catlid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ℎ ) = ℎ )
33 29 31 32 3eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ) = ℎ )
34 28 33 eqeq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) ) = ( 𝐺 ( ⟨ 𝑥 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) ) ↔ 𝑔 = ℎ ) )
35 14 34 syl5ib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
36 35 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
37 36 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
38 1 8 9 2 4 5 6 ismon2 ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑋 ) ( ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝐹 ( ⟨ 𝑥 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
39 13 37 38 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝑀 𝑌 ) )