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	$⊢ B = {Base}_{C}$
	sectmon.m	$⊢ M = Mono (C)$
	sectmon.s	$⊢ S = Sect (C)$
	sectmon.c	$⊢ φ \to C \in Cat$
	sectmon.x	$⊢ φ \to X \in B$
	sectmon.y	$⊢ φ \to Y \in B$
	sectmon.1	$⊢ φ \to F (X S Y) G$
Assertion	sectmon	$⊢ φ \to F \in (X M Y)$

Proof

Step	Hyp	Ref	Expression
1		sectmon.b	$⊢ B = {Base}_{C}$
2		sectmon.m	$⊢ M = Mono (C)$
3		sectmon.s	$⊢ S = Sect (C)$
4		sectmon.c	$⊢ φ \to C \in Cat$
5		sectmon.x	$⊢ φ \to X \in B$
6		sectmon.y	$⊢ φ \to Y \in B$
7		sectmon.1	$⊢ φ \to F (X S Y) G$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1 8 9 10 3 4 5 6	issect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
12	7 11	mpbid	$⊢ φ \to (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
13	12	simp1d	$⊢ φ \to F \in (X Hom (C) Y)$
14		oveq2	$⊢ F (⟨x, X⟩ comp (C) Y) g = F (⟨x, X⟩ comp (C) Y) h \to G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) g) = G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) h)$
15	12	simp3d	$⊢ φ \to G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)$
16	15	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)$
17	16	oveq1d	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (G (⟨X, Y⟩ comp (C) X) F) (⟨x, X⟩ comp (C) X) g = Id (C) (X) (⟨x, X⟩ comp (C) X) g$
18	4	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to C \in Cat$
19		simplr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to x \in B$
20	5	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to X \in B$
21	6	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to Y \in B$
22		simprl	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to g \in (x Hom (C) X)$
23	13	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to F \in (X Hom (C) Y)$
24	12	simp2d	$⊢ φ \to G \in (Y Hom (C) X)$
25	24	ad2antrr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to G \in (Y Hom (C) X)$
26	1 8 9 18 19 20 21 22 23 20 25	catass	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (G (⟨X, Y⟩ comp (C) X) F) (⟨x, X⟩ comp (C) X) g = G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) g)$
27	1 8 10 18 19 9 20 22	catlid	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to Id (C) (X) (⟨x, X⟩ comp (C) X) g = g$
28	17 26 27	3eqtr3d	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) g) = g$
29	16	oveq1d	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (G (⟨X, Y⟩ comp (C) X) F) (⟨x, X⟩ comp (C) X) h = Id (C) (X) (⟨x, X⟩ comp (C) X) h$
30		simprr	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to h \in (x Hom (C) X)$
31	1 8 9 18 19 20 21 30 23 20 25	catass	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (G (⟨X, Y⟩ comp (C) X) F) (⟨x, X⟩ comp (C) X) h = G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) h)$
32	1 8 10 18 19 9 20 30	catlid	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to Id (C) (X) (⟨x, X⟩ comp (C) X) h = h$
33	29 31 32	3eqtr3d	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) h) = h$
34	28 33	eqeq12d	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) g) = G (⟨x, Y⟩ comp (C) X) (F (⟨x, X⟩ comp (C) Y) h) \leftrightarrow g = h)$
35	14 34	imbitrid	$⊢ ((φ \land x \in B) \land (g \in (x Hom (C) X) \land h \in (x Hom (C) X))) \to (F (⟨x, X⟩ comp (C) Y) g = F (⟨x, X⟩ comp (C) Y) h \to g = h)$
36	35	ralrimivva	$⊢ (φ \land x \in B) \to \forall g \in (x Hom (C) X) \forall h \in (x Hom (C) X) (F (⟨x, X⟩ comp (C) Y) g = F (⟨x, X⟩ comp (C) Y) h \to g = h)$
37	36	ralrimiva	$⊢ φ \to \forall x \in B \forall g \in (x Hom (C) X) \forall h \in (x Hom (C) X) (F (⟨x, X⟩ comp (C) Y) g = F (⟨x, X⟩ comp (C) Y) h \to g = h)$
38	1 8 9 2 4 5 6	ismon2	$⊢ φ \to (F \in (X M Y) \leftrightarrow (F \in (X Hom (C) Y) \land \forall x \in B \forall g \in (x Hom (C) X) \forall h \in (x Hom (C) X) (F (⟨x, X⟩ comp (C) Y) g = F (⟨x, X⟩ comp (C) Y) h \to g = h)))$
39	13 37 38	mpbir2and	$⊢ φ \to F \in (X M Y)$

Metamath Proof Explorer

Theorem sectmon

Proof