| 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 |
|
grpmnd |
⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd ) |
| 54 |
29 53
|
syl |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Mnd ) |
| 55 |
2 1
|
lsmssv |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑅 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 56 |
54 32 37 55
|
syl3anc |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 57 |
2 3 1
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑅 ⊕ 𝑇 ) ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ) ) |
| 58 |
29 56 42 57
|
syl3anc |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ ( 𝑅 ⊕ 𝑇 ) ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑐 ) ) ) |
| 59 |
2 1
|
lsmssv |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 60 |
54 37 42 59
|
syl3anc |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 61 |
2 3 1
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑅 ⊆ ( Base ‘ 𝐺 ) ∧ ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
| 62 |
29 32 60 61
|
syl3anc |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ↔ ∃ 𝑎 ∈ 𝑅 ∃ 𝑧 ∈ ( 𝑇 ⊕ 𝑈 ) 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑧 ) ) ) |
| 63 |
52 58 62
|
3bitr4d |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑥 ∈ ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) ↔ 𝑥 ∈ ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ) ) |
| 64 |
63
|
eqrdv |
⊢ ( ( 𝑅 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑅 ⊕ 𝑇 ) ⊕ 𝑈 ) = ( 𝑅 ⊕ ( 𝑇 ⊕ 𝑈 ) ) ) |