lsmass

Description: Subgroup sum is associative. (Contributed by NM, 2-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

		Ref	Expression
	Hypothesis	lsmub1.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmass	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (R \underset{˙}{\oplus} T) \underset{˙}{\oplus} U = R \underset{˙}{\oplus} (T \underset{˙}{\oplus} 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	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G)) \to R \underset{˙}{\oplus} T = ran (a \in R, b \in T ⟼ a +_{G} b)$
5	4	3adant3	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to R \underset{˙}{\oplus} T = ran (a \in R, b \in T ⟼ a +_{G} b)$
6	5	rexeqdv	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists y \in (R \underset{˙}{\oplus} T) \exists c \in U x = y +_{G} c \leftrightarrow \exists y \in ran (a \in R, b \in T ⟼ a +_{G} b) \exists c \in U x = y +_{G} c)$
7		ovex	$⊢ a +_{G} b \in V$
8	7	rgen2w	$⊢ \forall a \in R \forall b \in T a +_{G} b \in V$
9		eqid	$⊢ (a \in R, b \in T ⟼ a +_{G} b) = (a \in R, b \in T ⟼ a +_{G} b)$
10		oveq1	$⊢ y = a +_{G} b \to y +_{G} c = (a +_{G} b) +_{G} c$
11	10	eqeq2d	$⊢ y = a +_{G} b \to (x = y +_{G} c \leftrightarrow x = (a +_{G} b) +_{G} c)$
12	11	rexbidv	$⊢ y = a +_{G} b \to (\exists c \in U x = y +_{G} c \leftrightarrow \exists c \in U x = (a +_{G} b) +_{G} c)$
13	9 12	rexrnmpo	$⊢ \forall a \in R \forall b \in T a +_{G} b \in V \to (\exists y \in ran (a \in R, b \in T ⟼ a +_{G} b) \exists c \in U x = y +_{G} c \leftrightarrow \exists a \in R \exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c)$
14	8 13	ax-mp	$⊢ \exists y \in ran (a \in R, b \in T ⟼ a +_{G} b) \exists c \in U x = y +_{G} c \leftrightarrow \exists a \in R \exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c$
15	6 14	bitrdi	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists y \in (R \underset{˙}{\oplus} T) \exists c \in U x = y +_{G} c \leftrightarrow \exists a \in R \exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c)$
16	2 3 1	lsmval	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to T \underset{˙}{\oplus} U = ran (b \in T, c \in U ⟼ b +_{G} c)$
17	16	3adant1	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \underset{˙}{\oplus} U = ran (b \in T, c \in U ⟼ b +_{G} c)$
18	17	rexeqdv	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z \leftrightarrow \exists z \in ran (b \in T, c \in U ⟼ b +_{G} c) x = a +_{G} z)$
19		ovex	$⊢ b +_{G} c \in V$
20	19	rgen2w	$⊢ \forall b \in T \forall c \in U b +_{G} c \in V$
21		eqid	$⊢ (b \in T, c \in U ⟼ b +_{G} c) = (b \in T, c \in U ⟼ b +_{G} c)$
22		oveq2	$⊢ z = b +_{G} c \to a +_{G} z = a +_{G} (b +_{G} c)$
23	22	eqeq2d	$⊢ z = b +_{G} c \to (x = a +_{G} z \leftrightarrow x = a +_{G} (b +_{G} c))$
24	21 23	rexrnmpo	$⊢ \forall b \in T \forall c \in U b +_{G} c \in V \to (\exists z \in ran (b \in T, c \in U ⟼ b +_{G} c) x = a +_{G} z \leftrightarrow \exists b \in T \exists c \in U x = a +_{G} (b +_{G} c))$
25	20 24	ax-mp	$⊢ \exists z \in ran (b \in T, c \in U ⟼ b +_{G} c) x = a +_{G} z \leftrightarrow \exists b \in T \exists c \in U x = a +_{G} (b +_{G} c)$
26	18 25	bitrdi	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z \leftrightarrow \exists b \in T \exists c \in U x = a +_{G} (b +_{G} c))$
27	26	adantr	$⊢ ((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \to (\exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z \leftrightarrow \exists b \in T \exists c \in U x = a +_{G} (b +_{G} c))$
28		subgrcl	$⊢ R \in SubGrp (G) \to G \in Grp$
29	28	3ad2ant1	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to G \in Grp$
30	29	ad2antrr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to G \in Grp$
31	2	subgss	$⊢ R \in SubGrp (G) \to R \subseteq {Base}_{G}$
32	31	3ad2ant1	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to R \subseteq {Base}_{G}$
33	32	ad2antrr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to R \subseteq {Base}_{G}$
34		simplr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to a \in R$
35	33 34	sseldd	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to a \in {Base}_{G}$
36	2	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
37	36	3ad2ant2	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \subseteq {Base}_{G}$
38	37	ad2antrr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to T \subseteq {Base}_{G}$
39		simprl	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to b \in T$
40	38 39	sseldd	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to b \in {Base}_{G}$
41	2	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
42	41	3ad2ant3	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to U \subseteq {Base}_{G}$
43	42	ad2antrr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to U \subseteq {Base}_{G}$
44		simprr	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to c \in U$
45	43 44	sseldd	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to c \in {Base}_{G}$
46	2 3	grpass	$⊢ (G \in Grp \land (a \in {Base}_{G} \land b \in {Base}_{G} \land c \in {Base}_{G})) \to (a +_{G} b) +_{G} c = a +_{G} (b +_{G} c)$
47	30 35 40 45 46	syl13anc	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to (a +_{G} b) +_{G} c = a +_{G} (b +_{G} c)$
48	47	eqeq2d	$⊢ (((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \land (b \in T \land c \in U)) \to (x = (a +_{G} b) +_{G} c \leftrightarrow x = a +_{G} (b +_{G} c))$
49	48	2rexbidva	$⊢ ((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \to (\exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c \leftrightarrow \exists b \in T \exists c \in U x = a +_{G} (b +_{G} c))$
50	27 49	bitr4d	$⊢ ((R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land a \in R) \to (\exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z \leftrightarrow \exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c)$
51	50	rexbidva	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists a \in R \exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z \leftrightarrow \exists a \in R \exists b \in T \exists c \in U x = (a +_{G} b) +_{G} c)$
52	15 51	bitr4d	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (\exists y \in (R \underset{˙}{\oplus} T) \exists c \in U x = y +_{G} c \leftrightarrow \exists a \in R \exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z)$
53	29	grpmndd	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to G \in Mnd$
54	2 1	lsmssv	$⊢ (G \in Mnd \land R \subseteq {Base}_{G} \land T \subseteq {Base}_{G}) \to R \underset{˙}{\oplus} T \subseteq {Base}_{G}$
55	53 32 37 54	syl3anc	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to R \underset{˙}{\oplus} T \subseteq {Base}_{G}$
56	2 3 1	lsmelvalx	$⊢ (G \in Grp \land R \underset{˙}{\oplus} T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to (x \in ((R \underset{˙}{\oplus} T) \underset{˙}{\oplus} U) \leftrightarrow \exists y \in (R \underset{˙}{\oplus} T) \exists c \in U x = y +_{G} c)$
57	29 55 42 56	syl3anc	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in ((R \underset{˙}{\oplus} T) \underset{˙}{\oplus} U) \leftrightarrow \exists y \in (R \underset{˙}{\oplus} T) \exists c \in U x = y +_{G} c)$
58	2 1	lsmssv	$⊢ (G \in Mnd \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
59	53 37 42 58	syl3anc	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to T \underset{˙}{\oplus} U \subseteq {Base}_{G}$
60	2 3 1	lsmelvalx	$⊢ (G \in Grp \land R \subseteq {Base}_{G} \land T \underset{˙}{\oplus} U \subseteq {Base}_{G}) \to (x \in (R \underset{˙}{\oplus} (T \underset{˙}{\oplus} U)) \leftrightarrow \exists a \in R \exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z)$
61	29 32 59 60	syl3anc	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in (R \underset{˙}{\oplus} (T \underset{˙}{\oplus} U)) \leftrightarrow \exists a \in R \exists z \in (T \underset{˙}{\oplus} U) x = a +_{G} z)$
62	52 57 61	3bitr4d	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (x \in ((R \underset{˙}{\oplus} T) \underset{˙}{\oplus} U) \leftrightarrow x \in (R \underset{˙}{\oplus} (T \underset{˙}{\oplus} U)))$
63	62	eqrdv	$⊢ (R \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \to (R \underset{˙}{\oplus} T) \underset{˙}{\oplus} U = R \underset{˙}{\oplus} (T \underset{˙}{\oplus} U)$

Metamath Proof Explorer

Theorem lsmass

Proof