Theorem lsmss1

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	lsmss1	⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑇 ⊆ 𝑈 ) → ( 𝑇 ⊕ 𝑈 ) = 𝑈 )

Proof

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