submefmnd

Description: If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set A , contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set A . Analogous to pgrpsubgsymg . (Contributed by AV, 17-Feb-2024)

	Ref	Expression
Hypotheses	submefmnd.g	No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
	submefmnd.b	$⊢ B = {Base}_{M}$
	submefmnd.0	$⊢ \underset{˙}{0} = 0_{M}$
	submefmnd.c	$⊢ F = {Base}_{S}$
Assertion	submefmnd	$⊢ A \in V \to (((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to F \in SubMnd (M))$

Proof

Step	Hyp	Ref	Expression
1		submefmnd.g	Could not format M = ( EndoFMnd ` A ) : No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
2		submefmnd.b	$⊢ B = {Base}_{M}$
3		submefmnd.0	$⊢ \underset{˙}{0} = 0_{M}$
4		submefmnd.c	$⊢ F = {Base}_{S}$
5	1	efmndmnd	$⊢ A \in V \to M \in Mnd$
6		simpl1	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to S \in Mnd$
7	5 6	anim12i	$⊢ (A \in V \land ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g))) \to (M \in Mnd \land S \in Mnd)$
8		simpl2	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to F \subseteq B$
9		simpl3	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to \underset{˙}{0} \in F$
10		simpr	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to +_{S} = (f \in F, g \in F ⟼ f \circ g)$
11		eqid	$⊢ +_{M} = +_{M}$
12	1 2 11	efmndplusg	$⊢ +_{M} = (f \in B, g \in B ⟼ f \circ g)$
13	12	eqcomi	$⊢ (f \in B, g \in B ⟼ f \circ g) = +_{M}$
14	13	reseq1i	$⊢ {(f \in B, g \in B ⟼ f \circ g) ↾}_{(F \times F)} = {+_{M} ↾}_{(F \times F)}$
15		resmpo	$⊢ (F \subseteq B \land F \subseteq B) \to {(f \in B, g \in B ⟼ f \circ g) ↾}_{(F \times F)} = (f \in F, g \in F ⟼ f \circ g)$
16	15	anidms	$⊢ F \subseteq B \to {(f \in B, g \in B ⟼ f \circ g) ↾}_{(F \times F)} = (f \in F, g \in F ⟼ f \circ g)$
17	14 16	syl5reqr	$⊢ F \subseteq B \to (f \in F, g \in F ⟼ f \circ g) = {+_{M} ↾}_{(F \times F)}$
18	17	3ad2ant2	$⊢ (S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \to (f \in F, g \in F ⟼ f \circ g) = {+_{M} ↾}_{(F \times F)}$
19	18	adantr	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to (f \in F, g \in F ⟼ f \circ g) = {+_{M} ↾}_{(F \times F)}$
20	10 19	eqtrd	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to +_{S} = {+_{M} ↾}_{(F \times F)}$
21	8 9 20	3jca	$⊢ ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to (F \subseteq B \land \underset{˙}{0} \in F \land +_{S} = {+_{M} ↾}_{(F \times F)})$
22	21	adantl	$⊢ (A \in V \land ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g))) \to (F \subseteq B \land \underset{˙}{0} \in F \land +_{S} = {+_{M} ↾}_{(F \times F)})$
23	2 4 3	mndissubm	$⊢ (M \in Mnd \land S \in Mnd) \to ((F \subseteq B \land \underset{˙}{0} \in F \land +_{S} = {+_{M} ↾}_{(F \times F)}) \to F \in SubMnd (M))$
24	7 22 23	sylc	$⊢ (A \in V \land ((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g))) \to F \in SubMnd (M)$
25	24	ex	$⊢ A \in V \to (((S \in Mnd \land F \subseteq B \land \underset{˙}{0} \in F) \land +_{S} = (f \in F, g \in F ⟼ f \circ g)) \to F \in SubMnd (M))$

Metamath Proof Explorer

Theorem submefmnd

Proof