Description: Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lsmval.v | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
lsmval.a | ⊢ + = ( +g ‘ 𝐺 ) | ||
lsmval.p | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | ||
Assertion | lsmval | ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lsmval.v | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
2 | lsmval.a | ⊢ + = ( +g ‘ 𝐺 ) | |
3 | lsmval.p | ⊢ ⊕ = ( LSSum ‘ 𝐺 ) | |
4 | subgrcl | ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) | |
5 | 1 | subgss | ⊢ ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) → 𝑇 ⊆ 𝐵 ) |
6 | 1 | subgss | ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 ) |
7 | 1 2 3 | lsmvalx | ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ) |
8 | 4 5 6 7 | syl2an3an | ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 + 𝑦 ) ) ) |