| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lsmsubg.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
| 2 |
|
lsmsubg.z |
⊢ 𝑍 = ( Cntz ‘ 𝐺 ) |
| 3 |
|
submrcl |
⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd ) |
| 4 |
3
|
3ad2ant1 |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝐺 ∈ Mnd ) |
| 5 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
| 6 |
5
|
submss |
⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
| 7 |
6
|
3ad2ant1 |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
| 8 |
5
|
submss |
⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
| 9 |
8
|
3ad2ant2 |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
| 10 |
5 1
|
lsmssv |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 11 |
4 7 9 10
|
syl3anc |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ) |
| 12 |
|
simp2 |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ) |
| 13 |
5 1
|
lsmub1x |
⊢ ( ( 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
| 14 |
7 12 13
|
syl2anc |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ) |
| 15 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
| 16 |
15
|
subm0cl |
⊢ ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑇 ) |
| 17 |
16
|
3ad2ant1 |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 0g ‘ 𝐺 ) ∈ 𝑇 ) |
| 18 |
14 17
|
sseldd |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 0g ‘ 𝐺 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
| 19 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
| 20 |
5 19 1
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑎 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) ) |
| 21 |
4 7 9 20
|
syl3anc |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑎 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ) ) |
| 22 |
5 19 1
|
lsmelvalx |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 23 |
4 7 9 22
|
syl3anc |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑏 ∈ 𝑇 ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 24 |
21 23
|
anbi12d |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) ↔ ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑏 ∈ 𝑇 ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) ) |
| 25 |
|
reeanv |
⊢ ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑏 ∈ 𝑇 ( ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ↔ ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑏 ∈ 𝑇 ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 26 |
|
reeanv |
⊢ ( ∃ 𝑐 ∈ 𝑈 ∃ 𝑑 ∈ 𝑈 ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ↔ ( ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 27 |
4
|
adantr |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝐺 ∈ Mnd ) |
| 28 |
7
|
adantr |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
| 29 |
|
simprll |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑎 ∈ 𝑇 ) |
| 30 |
28 29
|
sseldd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑎 ∈ ( Base ‘ 𝐺 ) ) |
| 31 |
|
simprlr |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑏 ∈ 𝑇 ) |
| 32 |
28 31
|
sseldd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑏 ∈ ( Base ‘ 𝐺 ) ) |
| 33 |
9
|
adantr |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
| 34 |
|
simprrl |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑐 ∈ 𝑈 ) |
| 35 |
33 34
|
sseldd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑐 ∈ ( Base ‘ 𝐺 ) ) |
| 36 |
|
simprrr |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑑 ∈ 𝑈 ) |
| 37 |
33 36
|
sseldd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑑 ∈ ( Base ‘ 𝐺 ) ) |
| 38 |
|
simpl3 |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) |
| 39 |
38 31
|
sseldd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑏 ∈ ( 𝑍 ‘ 𝑈 ) ) |
| 40 |
19 2
|
cntzi |
⊢ ( ( 𝑏 ∈ ( 𝑍 ‘ 𝑈 ) ∧ 𝑐 ∈ 𝑈 ) → ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) = ( 𝑐 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 41 |
39 34 40
|
syl2anc |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( 𝑏 ( +g ‘ 𝐺 ) 𝑐 ) = ( 𝑐 ( +g ‘ 𝐺 ) 𝑏 ) ) |
| 42 |
5 19 27 30 32 35 37 41
|
mnd4g |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ) = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 43 |
|
simpl1 |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ) |
| 44 |
19
|
submcl |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑇 ) |
| 45 |
43 29 31 44
|
syl3anc |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑇 ) |
| 46 |
|
simpl2 |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ) |
| 47 |
19
|
submcl |
⊢ ( ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) → ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑈 ) |
| 48 |
46 34 36 47
|
syl3anc |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑈 ) |
| 49 |
5 19 1
|
lsmelvalix |
⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ∈ 𝑇 ∧ ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ∈ 𝑈 ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
| 50 |
27 28 33 45 48 49
|
syl32anc |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑐 ( +g ‘ 𝐺 ) 𝑑 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
| 51 |
42 50
|
eqeltrrd |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
| 52 |
|
oveq12 |
⊢ ( ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ) |
| 53 |
52
|
eleq1d |
⊢ ( ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ( +g ‘ 𝐺 ) ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 54 |
51 53
|
syl5ibrcom |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) ) → ( ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 55 |
54
|
anassrs |
⊢ ( ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝑈 ∧ 𝑑 ∈ 𝑈 ) ) → ( ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 56 |
55
|
rexlimdvva |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ) → ( ∃ 𝑐 ∈ 𝑈 ∃ 𝑑 ∈ 𝑈 ( 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 57 |
26 56
|
biimtrrid |
⊢ ( ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) ∧ ( 𝑎 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ) ) → ( ( ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 58 |
57
|
rexlimdvva |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑏 ∈ 𝑇 ( ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 59 |
25 58
|
biimtrrid |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ( ∃ 𝑎 ∈ 𝑇 ∃ 𝑐 ∈ 𝑈 𝑥 = ( 𝑎 ( +g ‘ 𝐺 ) 𝑐 ) ∧ ∃ 𝑏 ∈ 𝑇 ∃ 𝑑 ∈ 𝑈 𝑦 = ( 𝑏 ( +g ‘ 𝐺 ) 𝑑 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 60 |
24 59
|
sylbid |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) |
| 61 |
60
|
ralrimivv |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
| 62 |
5 15 19
|
issubm |
⊢ ( 𝐺 ∈ Mnd → ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) ) |
| 63 |
4 62
|
syl |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝑇 ⊕ 𝑈 ) ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ ( 𝑇 ⊕ 𝑈 ) ∧ ∀ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∀ 𝑦 ∈ ( 𝑇 ⊕ 𝑈 ) ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) ) ) |
| 64 |
11 18 61 63
|
mpbir3and |
⊢ ( ( 𝑇 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ ( SubMnd ‘ 𝐺 ) ) |