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

Metamath Proof Explorer

Theorem lsmssv

Description: Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmless2.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
lsmless2.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmssv ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 lsmless2.v ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 lsmless2.s ⊢ ⊕ = ( LSSum ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 1 3 2 lsmvalx ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) = ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) )
5 simpl1 ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) ) → 𝐺 ∈ Mnd )
6 simp2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑇 ⊆ 𝐵 )
7 6 sselda ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ 𝐵 )
8 7 adantrr ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑥 ∈ 𝐵 )
9 simp3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → 𝑈 ⊆ 𝐵 )
10 9 sselda ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ 𝐵 )
11 10 adantrl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝐵 )
12 1 3 mndcl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
13 5 8 11 12 syl3anc ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ 𝑇 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
14 13 ralrimivva ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝑇 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
15 eqid ⊢ ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
16 15 fmpo ⊢ ( ∀ 𝑥 ∈ 𝑇 ∀ 𝑦 ∈ 𝑈 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑇 × 𝑈 ) ⟶ 𝐵 )
17 14 16 sylib ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) : ( 𝑇 × 𝑈 ) ⟶ 𝐵 )
18 17 frnd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ran ( 𝑥 ∈ 𝑇 , 𝑦 ∈ 𝑈 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) ⊆ 𝐵 )
19 4 18 eqsstrd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 )