Description: Subgroup sum commutes. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | lsmcom.s | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | |
| Assertion | lsmcom | ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsmcom.s | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | |
| 2 | id | ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Abel ) | |
| 3 | eqid | ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) | |
| 4 | 3 | subgss | ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ ( Base ‘ 𝐺 ) ) |
| 5 | 3 | subgss | ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ ( Base ‘ 𝐺 ) ) |
| 6 | 3 1 | lsmcomx | ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑈 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) ) |
| 7 | 2 4 5 6 | syl3an | ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ( 𝑈 ⊕ 𝑇 ) ) |