Step |
Hyp |
Ref |
Expression |
1 |
|
lsmelval.a |
⊢ + = ( +g ‘ 𝐺 ) |
2 |
|
lsmelval.p |
⊢ ⊕ = ( LSSum ‘ 𝐺 ) |
3 |
|
subgrcl |
⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
4 |
3
|
adantr |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
6 |
5
|
subgss |
⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
8 |
5
|
subgss |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
9 |
8
|
adantl |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
10 |
4 7 9
|
3jca |
⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ) |
11 |
5 1 2
|
lsmelvalix |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |
12 |
10 11
|
sylan |
⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) ) |