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 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝐵 )