Theorem lsmless2x

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

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

Proof

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