Metamath Proof Explorer

Theorem lsmless12

Description: Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p ⊢ ⊕ ˙ = LSSum ⁡ G
Assertion lsmless12 ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → R ⊕ ˙ T ⊆ S ⊕ ˙ U

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ ˙ = LSSum ⁡ G
2 subgrcl ⊢ S ∈ SubGrp ⁡ G → G ∈ Grp
3 2 ad2antrr ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → G ∈ Grp
4 eqid ⊢ Base G = Base G
5 4 subgss ⊢ S ∈ SubGrp ⁡ G → S ⊆ Base G
6 5 ad2antrr ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → S ⊆ Base G
7 simprr ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → T ⊆ U
8 4 subgss ⊢ U ∈ SubGrp ⁡ G → U ⊆ Base G
9 8 ad2antlr ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → U ⊆ Base G
10 7 9 sstrd ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → T ⊆ Base G
11 simprl ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → R ⊆ S
12 4 1 lsmless1x ⊢ G ∈ Grp ∧ S ⊆ Base G ∧ T ⊆ Base G ∧ R ⊆ S → R ⊕ ˙ T ⊆ S ⊕ ˙ T
13 3 6 10 11 12 syl31anc ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → R ⊕ ˙ T ⊆ S ⊕ ˙ T
14 simpll ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → S ∈ SubGrp ⁡ G
15 simplr ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → U ∈ SubGrp ⁡ G
16 1 lsmless2 ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ T ⊆ U → S ⊕ ˙ T ⊆ S ⊕ ˙ U
17 14 15 7 16 syl3anc ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → S ⊕ ˙ T ⊆ S ⊕ ˙ U
18 13 17 sstrd ⊢ S ∈ SubGrp ⁡ G ∧ U ∈ SubGrp ⁡ G ∧ R ⊆ S ∧ T ⊆ U → R ⊕ ˙ T ⊆ S ⊕ ˙ U