Theorem lsmless1x

Description: Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 22-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		lsmless2.v	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		lsmless2.s	⊢ ⊕ = ( LSSum ‘ 𝐺 )
3		ssrexv	⊢ ( 𝑅 ⊆ 𝑇 → ( ∃ 𝑦 ∈ 𝑅 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
4	3	adantl	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → ( ∃ 𝑦 ∈ 𝑅 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
5		simpl1	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → 𝐺 ∈ 𝑉 )
6		simpr	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → 𝑅 ⊆ 𝑇 )
7		simpl2	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → 𝑇 ⊆ 𝐵 )
8	6 7	sstrd	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → 𝑅 ⊆ 𝐵 )
9		simpl3	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → 𝑈 ⊆ 𝐵 )
10		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11	1 10 2	lsmelvalx	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑅 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑅 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑅 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
12	5 8 9 11	syl3anc	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → ( 𝑥 ∈ ( 𝑅 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑅 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
13	1 10 2	lsmelvalx	⊢ ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
14	13	adantr	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
15	4 12 14	3imtr4d	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → ( 𝑥 ∈ ( 𝑅 ⊕ 𝑈 ) → 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ) )
16	15	ssrdv	⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑅 ⊆ 𝑇 ) → ( 𝑅 ⊕ 𝑈 ) ⊆ ( 𝑇 ⊕ 𝑈 ) )