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

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ 𝑅 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑅 ⊕ 𝑇 ) ⊆ ( 𝑅 ⊕ 𝑈 ) )