lsmcom2

Description: Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016)

	Ref	Expression
Hypotheses	lsmsubg.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmsubg.z	$⊢ Z = Cntz (G)$
Assertion	lsmcom2	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$

Proof

Step	Hyp	Ref	Expression
1		lsmsubg.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmsubg.z	$⊢ Z = Cntz (G)$
3		simp3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \subseteq Z (U)$
4	3	sselda	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land a \in T) \to a \in Z (U)$
5	4	adantrr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to a \in Z (U)$
6		simprr	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to b \in U$
7		eqid	$⊢ +_{G} = +_{G}$
8	7 2	cntzi	$⊢ (a \in Z (U) \land b \in U) \to a +_{G} b = b +_{G} a$
9	5 6 8	syl2anc	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to a +_{G} b = b +_{G} a$
10	9	eqeq2d	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \land (a \in T \land b \in U)) \to (x = a +_{G} b \leftrightarrow x = b +_{G} a)$
11	10	2rexbidva	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (\exists a \in T \exists b \in U x = a +_{G} b \leftrightarrow \exists a \in T \exists b \in U x = b +_{G} a)$
12		rexcom	$⊢ \exists a \in T \exists b \in U x = b +_{G} a \leftrightarrow \exists b \in U \exists a \in T x = b +_{G} a$
13	11 12	bitrdi	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (\exists a \in T \exists b \in U x = a +_{G} b \leftrightarrow \exists b \in U \exists a \in T x = b +_{G} a)$
14	7 1	lsmelval	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists b \in U x = a +_{G} b)$
15	14	3adant3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists a \in T \exists b \in U x = a +_{G} b)$
16	7 1	lsmelval	$⊢ (U \in SubGrp (G) \land T \in SubGrp (G)) \to (x \in (U \underset{˙}{\oplus} T) \leftrightarrow \exists b \in U \exists a \in T x = b +_{G} a)$
17	16	ancoms	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in (U \underset{˙}{\oplus} T) \leftrightarrow \exists b \in U \exists a \in T x = b +_{G} a)$
18	17	3adant3	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (x \in (U \underset{˙}{\oplus} T) \leftrightarrow \exists b \in U \exists a \in T x = b +_{G} a)$
19	13 15 18	3bitr4d	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to (x \in (T \underset{˙}{\oplus} U) \leftrightarrow x \in (U \underset{˙}{\oplus} T))$
20	19	eqrdv	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G) \land T \subseteq Z (U)) \to T \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$

Metamath Proof Explorer

Theorem lsmcom2

Proof