Metamath Proof Explorer

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

Proof

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