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	$⊢ M = EndoFMnd (A)$
	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	$⊢ M = EndoFMnd (A)$
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		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)$
12	11	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)$
13		eqid	$⊢ +_{M} = +_{M}$
14	1 2 13	efmndplusg	$⊢ +_{M} = (f \in B, g \in B ⟼ f \circ g)$
15	14	eqcomi	$⊢ (f \in B, g \in B ⟼ f \circ g) = +_{M}$
16	15	reseq1i	$⊢ {(f \in B, g \in B ⟼ f \circ g) ↾}_{(F \times F)} = {+_{M} ↾}_{(F \times F)}$
17	12 16	eqtr3di	$⊢ 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