Metamath Proof Explorer

Theorem lsmub2x

Description: Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses lsmless2.v ⊢ B = Base G
lsmless2.s ⊢ ⊕ ˙ = LSSum ⁡ G
Assertion lsmub2x ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B → U ⊆ T ⊕ ˙ U

Proof

Step Hyp Ref Expression
1 lsmless2.v ⊢ B = Base G
2 lsmless2.s ⊢ ⊕ ˙ = LSSum ⁡ G
3 submrcl ⊢ T ∈ SubMnd ⁡ G → G ∈ Mnd
4 3 ad2antrr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → G ∈ Mnd
5 simpr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B → U ⊆ B
6 5 sselda ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → x ∈ B
7 eqid ⊢ + G = + G
8 eqid ⊢ 0 G = 0 G
9 1 7 8 mndlid ⊢ G ∈ Mnd ∧ x ∈ B → 0 G + G x = x
10 4 6 9 syl2anc ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → 0 G + G x = x
11 1 submss ⊢ T ∈ SubMnd ⁡ G → T ⊆ B
12 11 ad2antrr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → T ⊆ B
13 simplr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → U ⊆ B
14 8 subm0cl ⊢ T ∈ SubMnd ⁡ G → 0 G ∈ T
15 14 ad2antrr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → 0 G ∈ T
16 simpr ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → x ∈ U
17 1 7 2 lsmelvalix ⊢ G ∈ Mnd ∧ T ⊆ B ∧ U ⊆ B ∧ 0 G ∈ T ∧ x ∈ U → 0 G + G x ∈ T ⊕ ˙ U
18 4 12 13 15 16 17 syl32anc ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → 0 G + G x ∈ T ⊕ ˙ U
19 10 18 eqeltrrd ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B ∧ x ∈ U → x ∈ T ⊕ ˙ U
20 19 ex ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B → x ∈ U → x ∈ T ⊕ ˙ U
21 20 ssrdv ⊢ T ∈ SubMnd ⁡ G ∧ U ⊆ B → U ⊆ T ⊕ ˙ U