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
|
anidms |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ) |
6 |
3
|
subgcl |
⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 ) |
7 |
6
|
3expb |
⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 ) |
8 |
7
|
ralrimivva |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 ) |
9 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) |
10 |
9
|
fmpo |
⊢ ( ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑈 ↔ ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 ) |
11 |
8 10
|
sylib |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑈 × 𝑈 ) ⟶ 𝑈 ) |
12 |
11
|
frnd |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ran ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝑈 ) |
13 |
5 12
|
eqsstrd |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) ⊆ 𝑈 ) |
14 |
1
|
lsmub1 |
⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑈 ⊆ ( 𝑈 ⊕ 𝑈 ) ) |
15 |
14
|
anidms |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( 𝑈 ⊕ 𝑈 ) ) |
16 |
13 15
|
eqssd |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 ) |