This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmass

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

Ref Expression
Hypothesis lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmass ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) = ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) )

Proof

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