Metamath Proof Explorer

Theorem lsmss2

Description: Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014) (Revised by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion lsmss2 ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝑇 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑇 )

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 ssid ⊢ 𝑇 ⊆ 𝑇
3 1 lsmlub ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑇 ∧ 𝑈 ⊆ 𝑇 ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑇 ) )
4 3 3anidm13 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑇 ∧ 𝑈 ⊆ 𝑇 ) ↔ ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑇 ) )
5 4 biimpd ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊆ 𝑇 ∧ 𝑈 ⊆ 𝑇 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑇 ) )
6 2 5 mpani ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑈 ⊆ 𝑇 → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑇 ) )
7 6 3impia ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝑇 ) → ( 𝑇 ⊕ 𝑈 ) ⊆ 𝑇 )
8 1 lsmub1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
9 8 3adant3 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝑇 ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
10 7 9 eqssd ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ⊆ 𝑇 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑇 )