Metamath Proof Explorer

Theorem lsmidmOLD

Description: Obsolete proof of lsmidm as of 13-Jan-2024. Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		eqid	$⊢ {Base}_{G} = {Base}_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4	2 3 1	lsmval	$⊢ (U \in SubGrp (G) \land U \in SubGrp (G)) \to U \underset{˙}{\oplus} U = ran (x \in U, y \in U ⟼ x +_{G} y)$
5	4	anidms	$⊢ U \in SubGrp (G) \to U \underset{˙}{\oplus} U = ran (x \in U, y \in U ⟼ x +_{G} y)$
6	3	subgcl	$⊢ (U \in SubGrp (G) \land x \in U \land y \in U) \to x +_{G} y \in U$
7	6	3expb	$⊢ (U \in SubGrp (G) \land (x \in U \land y \in U)) \to x +_{G} y \in U$
8	7	ralrimivva	$⊢ U \in SubGrp (G) \to \forall x \in U \forall y \in U x +_{G} y \in U$
9		eqid	$⊢ (x \in U, y \in U ⟼ x +_{G} y) = (x \in U, y \in U ⟼ x +_{G} y)$
10	9	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$
11	8 10	sylib	$⊢ U \in SubGrp (G) \to (x \in U, y \in U ⟼ x +_{G} y) : U \times U ⟶ U$
12	11	frnd	$⊢ U \in SubGrp (G) \to ran (x \in U, y \in U ⟼ x +_{G} y) \subseteq U$
13	5 12	eqsstrd	$⊢ U \in SubGrp (G) \to U \underset{˙}{\oplus} U \subseteq U$
14	1	lsmub1	$⊢ (U \in SubGrp (G) \land U \in SubGrp (G)) \to U \subseteq U \underset{˙}{\oplus} U$
15	14	anidms	$⊢ U \in SubGrp (G) \to U \subseteq U \underset{˙}{\oplus} U$
16	13 15	eqssd	$⊢ U \in SubGrp (G) \to U \underset{˙}{\oplus} U = U$