This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmelvali

Description: Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmelval.a ⊢ + = ( +g ‘ 𝐺 )
lsmelval.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmelvali ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )

Proof

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 ‘ 𝐺 ) ) ∧ ( 𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑇 ⊕ 𝑈 ) )