This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmss1b

Description: Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015) (Revised by Mario Carneiro, 19-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 lsmub1.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
2 1 lsmss1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑈 )
3 2 3expia ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 → ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) )
4 1 lsmub1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) )
5 sseq2 ⊢ ( ( 𝑇 ⊕ 𝑈 ) = 𝑈 → ( 𝑇 ⊆ ( 𝑇 ⊕ 𝑈 ) ↔ 𝑇 ⊆ 𝑈 ) )
6 4 5 syl5ibcom ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑇 ⊕ 𝑈 ) = 𝑈 → 𝑇 ⊆ 𝑈 ) )
7 3 6 impbid ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑇 ⊆ 𝑈 ↔ ( 𝑇 ⊕ 𝑈 ) = 𝑈 ) )