lsmcomx

Description: Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmcomx.v	$⊢ B = {Base}_{G}$
	lsmcomx.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	lsmcomx	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$

Proof

Step	Hyp	Ref	Expression
1		lsmcomx.v	$⊢ B = {Base}_{G}$
2		lsmcomx.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		simpl1	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to G \in Abel$
4		simpl2	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to T \subseteq B$
5		simprl	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to y \in T$
6	4 5	sseldd	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to y \in B$
7		simpl3	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to U \subseteq B$
8		simprr	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to z \in U$
9	7 8	sseldd	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to z \in B$
10		eqid	$⊢ +_{G} = +_{G}$
11	1 10	ablcom	$⊢ (G \in Abel \land y \in B \land z \in B) \to y +_{G} z = z +_{G} y$
12	3 6 9 11	syl3anc	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to y +_{G} z = z +_{G} y$
13	12	eqeq2d	$⊢ ((G \in Abel \land T \subseteq B \land U \subseteq B) \land (y \in T \land z \in U)) \to (x = y +_{G} z \leftrightarrow x = z +_{G} y)$
14	13	2rexbidva	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to (\exists y \in T \exists z \in U x = y +_{G} z \leftrightarrow \exists y \in T \exists z \in U x = z +_{G} y)$
15		rexcom	$⊢ \exists y \in T \exists z \in U x = z +_{G} y \leftrightarrow \exists z \in U \exists y \in T x = z +_{G} y$
16	14 15	bitrdi	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to (\exists y \in T \exists z \in U x = y +_{G} z \leftrightarrow \exists z \in U \exists y \in T x = z +_{G} y)$
17	1 10 2	lsmelvalx	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U x = y +_{G} z)$
18	1 10 2	lsmelvalx	$⊢ (G \in Abel \land U \subseteq B \land T \subseteq B) \to (x \in (U \underset{˙}{\oplus} T) \leftrightarrow \exists z \in U \exists y \in T x = z +_{G} y)$
19	18	3com23	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to (x \in (U \underset{˙}{\oplus} T) \leftrightarrow \exists z \in U \exists y \in T x = z +_{G} y)$
20	16 17 19	3bitr4d	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow x \in (U \underset{˙}{\oplus} T))$
21	20	eqrdv	$⊢ (G \in Abel \land T \subseteq B \land U \subseteq B) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$

Metamath Proof Explorer

Theorem lsmcomx

Proof