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 ⊢ B = Base G
lsmless2.s ⊢ ⊕ ˙ = LSSum ⁡ G
Assertion lsmless2x ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → R ⊕ ˙ T ⊆ R ⊕ ˙ U

Proof

Step Hyp Ref Expression
1 lsmless2.v ⊢ B = Base G
2 lsmless2.s ⊢ ⊕ ˙ = LSSum ⁡ G
3 ssrexv ⊢ T ⊆ U → ∃ z ∈ T x = y + G z → ∃ z ∈ U x = y + G z
4 3 reximdv ⊢ T ⊆ U → ∃ y ∈ R ∃ z ∈ T x = y + G z → ∃ y ∈ R ∃ z ∈ U x = y + G z
5 4 adantl ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → ∃ y ∈ R ∃ z ∈ T x = y + G z → ∃ y ∈ R ∃ z ∈ U x = y + G z
6 simpl1 ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → G ∈ V
7 simpl2 ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → R ⊆ B
8 simpr ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → T ⊆ U
9 simpl3 ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → U ⊆ B
10 8 9 sstrd ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → T ⊆ B
11 eqid ⊢ + G = + G
12 1 11 2 lsmelvalx ⊢ G ∈ V ∧ R ⊆ B ∧ T ⊆ B → x ∈ R ⊕ ˙ T ↔ ∃ y ∈ R ∃ z ∈ T x = y + G z
13 6 7 10 12 syl3anc ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → x ∈ R ⊕ ˙ T ↔ ∃ y ∈ R ∃ z ∈ T x = y + G z
14 1 11 2 lsmelvalx ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B → x ∈ R ⊕ ˙ U ↔ ∃ y ∈ R ∃ z ∈ U x = y + G z
15 14 adantr ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → x ∈ R ⊕ ˙ U ↔ ∃ y ∈ R ∃ z ∈ U x = y + G z
16 5 13 15 3imtr4d ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → x ∈ R ⊕ ˙ T → x ∈ R ⊕ ˙ U
17 16 ssrdv ⊢ G ∈ V ∧ R ⊆ B ∧ U ⊆ B ∧ T ⊆ U → R ⊕ ˙ T ⊆ R ⊕ ˙ U