Theorem lsmass 19190

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

Hypothesis

Ref	Expression
lsmub1.p	⊢ ⊕ = (LSSum‘𝐺)

Assertion

Ref	Expression
lsmass	⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈)))

Proof of Theorem lsmass

Dummy variables 𝑥 𝑦 𝑎 𝑏 𝑐 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2738	. . . . . . . 8 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2738	. . . . . . . 8 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		lsmub1.p	. . . . . . . 8 ⊢ ⊕ = (LSSum‘𝐺)
4	1, 2, 3	lsmval 19168	. . . . . . 7 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺)) → (𝑅 ⊕ 𝑇) = ran (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏)))
5	4	3adant3 1130	. . . . . 6 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑅 ⊕ 𝑇) = ran (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏)))
6	5	rexeqdv 3340	. . . . 5 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑦 ∈ (𝑅 ⊕ 𝑇)∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑦 ∈ ran (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏))∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐)))
7		ovex 7288	. . . . . . 7 ⊢ (𝑎(+g‘𝐺)𝑏) ∈ V
8	7	rgen2w 3076	. . . . . 6 ⊢ ∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑇 (𝑎(+g‘𝐺)𝑏) ∈ V
9		eqid 2738	. . . . . . 7 ⊢ (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏)) = (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏))
10		oveq1 7262	. . . . . . . . 9 ⊢ (𝑦 = (𝑎(+g‘𝐺)𝑏) → (𝑦(+g‘𝐺)𝑐) = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐))
11	10	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑦 = (𝑎(+g‘𝐺)𝑏) → (𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
12	11	rexbidv 3225	. . . . . . 7 ⊢ (𝑦 = (𝑎(+g‘𝐺)𝑏) → (∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
13	9, 12	rexrnmpo 7391	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑅 ∀𝑏 ∈ 𝑇 (𝑎(+g‘𝐺)𝑏) ∈ V → (∃𝑦 ∈ ran (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏))∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
14	8, 13	ax-mp 5	. . . . 5 ⊢ (∃𝑦 ∈ ran (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑇 ↦ (𝑎(+g‘𝐺)𝑏))∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐))
15	6, 14	bitrdi 286	. . . 4 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑦 ∈ (𝑅 ⊕ 𝑇)∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
16	1, 2, 3	lsmval 19168	. . . . . . . . . 10 ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = ran (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐)))
17	16	3adant1 1128	. . . . . . . . 9 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = ran (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐)))
18	17	rexeqdv 3340	. . . . . . . 8 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑧 ∈ ran (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐))𝑥 = (𝑎(+g‘𝐺)𝑧)))
19		ovex 7288	. . . . . . . . . 10 ⊢ (𝑏(+g‘𝐺)𝑐) ∈ V
20	19	rgen2w 3076	. . . . . . . . 9 ⊢ ∀𝑏 ∈ 𝑇 ∀𝑐 ∈ 𝑈 (𝑏(+g‘𝐺)𝑐) ∈ V
21		eqid 2738	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐)) = (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐))
22		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑧 = (𝑏(+g‘𝐺)𝑐) → (𝑎(+g‘𝐺)𝑧) = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐)))
23	22	eqeq2d 2749	. . . . . . . . . 10 ⊢ (𝑧 = (𝑏(+g‘𝐺)𝑐) → (𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
24	21, 23	rexrnmpo 7391	. . . . . . . . 9 ⊢ (∀𝑏 ∈ 𝑇 ∀𝑐 ∈ 𝑈 (𝑏(+g‘𝐺)𝑐) ∈ V → (∃𝑧 ∈ ran (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐))𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
25	20, 24	ax-mp 5	. . . . . . . 8 ⊢ (∃𝑧 ∈ ran (𝑏 ∈ 𝑇, 𝑐 ∈ 𝑈 ↦ (𝑏(+g‘𝐺)𝑐))𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐)))
26	18, 25	bitrdi 286	. . . . . . 7 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
27	26	adantr 480	. . . . . 6 ⊢ (((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) → (∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
28		subgrcl 18675	. . . . . . . . . . 11 ⊢ (𝑅 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
29	28	3ad2ant1 1131	. . . . . . . . . 10 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Grp)
30	29	ad2antrr 722	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝐺 ∈ Grp)
31	1	subgss 18671	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ (SubGrp‘𝐺) → 𝑅 ⊆ (Base‘𝐺))
32	31	3ad2ant1 1131	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑅 ⊆ (Base‘𝐺))
33	32	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑅 ⊆ (Base‘𝐺))
34		simplr 765	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑎 ∈ 𝑅)
35	33, 34	sseldd 3918	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑎 ∈ (Base‘𝐺))
36	1	subgss 18671	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ (SubGrp‘𝐺) → 𝑇 ⊆ (Base‘𝐺))
37	36	3ad2ant2 1132	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑇 ⊆ (Base‘𝐺))
38	37	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑇 ⊆ (Base‘𝐺))
39		simprl 767	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑏 ∈ 𝑇)
40	38, 39	sseldd 3918	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑏 ∈ (Base‘𝐺))
41	1	subgss 18671	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ (Base‘𝐺))
42	41	3ad2ant3 1133	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑈 ⊆ (Base‘𝐺))
43	42	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑈 ⊆ (Base‘𝐺))
44		simprr 769	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑐 ∈ 𝑈)
45	43, 44	sseldd 3918	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → 𝑐 ∈ (Base‘𝐺))
46	1, 2	grpass 18501	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑎 ∈ (Base‘𝐺) ∧ 𝑏 ∈ (Base‘𝐺) ∧ 𝑐 ∈ (Base‘𝐺))) → ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐) = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐)))
47	30, 35, 40, 45, 46	syl13anc 1370	. . . . . . . 8 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐) = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐)))
48	47	eqeq2d 2749	. . . . . . 7 ⊢ ((((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) ∧ (𝑏 ∈ 𝑇 ∧ 𝑐 ∈ 𝑈)) → (𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐) ↔ 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
49	48	2rexbidva 3227	. . . . . 6 ⊢ (((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) → (∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = (𝑎(+g‘𝐺)(𝑏(+g‘𝐺)𝑐))))
50	27, 49	bitr4d 281	. . . . 5 ⊢ (((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑎 ∈ 𝑅) → (∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
51	50	rexbidva 3224	. . . 4 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑎 ∈ 𝑅 ∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧) ↔ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑇 ∃𝑐 ∈ 𝑈 𝑥 = ((𝑎(+g‘𝐺)𝑏)(+g‘𝐺)𝑐)))
52	15, 51	bitr4d 281	. . 3 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (∃𝑦 ∈ (𝑅 ⊕ 𝑇)∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑅 ∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧)))
53	29	grpmndd 18504	. . . . 5 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐺 ∈ Mnd)
54	1, 3	lsmssv 19163	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝑅 ⊆ (Base‘𝐺) ∧ 𝑇 ⊆ (Base‘𝐺)) → (𝑅 ⊕ 𝑇) ⊆ (Base‘𝐺))
55	53, 32, 37, 54	syl3anc 1369	. . . 4 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑅 ⊕ 𝑇) ⊆ (Base‘𝐺))
56	1, 2, 3	lsmelvalx 19160	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑅 ⊕ 𝑇) ⊆ (Base‘𝐺) ∧ 𝑈 ⊆ (Base‘𝐺)) → (𝑥 ∈ ((𝑅 ⊕ 𝑇) ⊕ 𝑈) ↔ ∃𝑦 ∈ (𝑅 ⊕ 𝑇)∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐)))
57	29, 55, 42, 56	syl3anc 1369	. . 3 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ ((𝑅 ⊕ 𝑇) ⊕ 𝑈) ↔ ∃𝑦 ∈ (𝑅 ⊕ 𝑇)∃𝑐 ∈ 𝑈 𝑥 = (𝑦(+g‘𝐺)𝑐)))
58	1, 3	lsmssv 19163	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ 𝑇 ⊆ (Base‘𝐺) ∧ 𝑈 ⊆ (Base‘𝐺)) → (𝑇 ⊕ 𝑈) ⊆ (Base‘𝐺))
59	53, 37, 42, 58	syl3anc 1369	. . . 4 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) ⊆ (Base‘𝐺))
60	1, 2, 3	lsmelvalx 19160	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ 𝑅 ⊆ (Base‘𝐺) ∧ (𝑇 ⊕ 𝑈) ⊆ (Base‘𝐺)) → (𝑥 ∈ (𝑅 ⊕ (𝑇 ⊕ 𝑈)) ↔ ∃𝑎 ∈ 𝑅 ∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧)))
61	29, 32, 59, 60	syl3anc 1369	. . 3 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ (𝑅 ⊕ (𝑇 ⊕ 𝑈)) ↔ ∃𝑎 ∈ 𝑅 ∃𝑧 ∈ (𝑇 ⊕ 𝑈)𝑥 = (𝑎(+g‘𝐺)𝑧)))
62	52, 57, 61	3bitr4d 310	. 2 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑥 ∈ ((𝑅 ⊕ 𝑇) ⊕ 𝑈) ↔ 𝑥 ∈ (𝑅 ⊕ (𝑇 ⊕ 𝑈))))
63	62	eqrdv 2736	1 ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  Vcvv 3422   ⊆ wss 3883  ran crn 5581  ‘cfv 6418  (class class class)co 7255   ∈ cmpo 7257  Basecbs 16840  +_gcplusg 16888  Mndcmnd 18300  Grpcgrp 18492  SubGrpcsubg 18664  LSSumclsm 19154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495  df-subg 18667  df-lsm 19156

This theorem is referenced by:  lsm4  19376  pgpfac1lem3  19595  idlsrgmnd  31561  lsatcvat3  36993