smndlsmidm

Description: The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023)

		Ref	Expression
	Hypothesis	lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	smndlsmidm	$⊢ U \in SubMnd (G) \to U \underset{˙}{\oplus} U = U$

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		elfvdm	$⊢ U \in SubMnd (G) \to G \in dom SubMnd$
3		eqid	$⊢ {Base}_{G} = {Base}_{G}$
4	3	submss	$⊢ U \in SubMnd (G) \to U \subseteq {Base}_{G}$
5		eqid	$⊢ +_{G} = +_{G}$
6	3 5 1	lsmvalx	$⊢ (G \in dom SubMnd \land U \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to U \underset{˙}{\oplus} U = ran (x \in U, y \in U ⟼ x +_{G} y)$
7	2 4 4 6	syl3anc	$⊢ U \in SubMnd (G) \to U \underset{˙}{\oplus} U = ran (x \in U, y \in U ⟼ x +_{G} y)$
8	5	submcl	$⊢ (U \in SubMnd (G) \land x \in U \land y \in U) \to x +_{G} y \in U$
9	8	3expb	$⊢ (U \in SubMnd (G) \land (x \in U \land y \in U)) \to x +_{G} y \in U$
10	9	ralrimivva	$⊢ U \in SubMnd (G) \to \forall x \in U \forall y \in U x +_{G} y \in U$
11		eqid	$⊢ (x \in U, y \in U ⟼ x +_{G} y) = (x \in U, y \in U ⟼ x +_{G} y)$
12	11	fmpo	$⊢ \forall x \in U \forall y \in U x +_{G} y \in U \leftrightarrow (x \in U, y \in U ⟼ x +_{G} y) : U \times U ⟶ U$
13	10 12	sylib	$⊢ U \in SubMnd (G) \to (x \in U, y \in U ⟼ x +_{G} y) : U \times U ⟶ U$
14	13	frnd	$⊢ U \in SubMnd (G) \to ran (x \in U, y \in U ⟼ x +_{G} y) \subseteq U$
15	7 14	eqsstrd	$⊢ U \in SubMnd (G) \to U \underset{˙}{\oplus} U \subseteq U$
16	3 1	lsmub1x	$⊢ (U \subseteq {Base}_{G} \land U \in SubMnd (G)) \to U \subseteq U \underset{˙}{\oplus} U$
17	4 16	mpancom	$⊢ U \in SubMnd (G) \to U \subseteq U \underset{˙}{\oplus} U$
18	15 17	eqssd	$⊢ U \in SubMnd (G) \to U \underset{˙}{\oplus} U = U$

Metamath Proof Explorer