Theorem subgsubcl

Description: A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015)

	Ref	Expression
Hypothesis	subgsubcl.p	⊢ − = ( -g ‘ 𝐺 )
Assertion	subgsubcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		subgsubcl.p	⊢ − = ( -g ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3	2	subgss	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
4	3	3ad2ant1	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
5		simp2	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
6	4 5	sseldd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
7		simp3	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
8	4 7	sseldd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ ( Base ‘ 𝐺 ) )
9		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
11	2 9 10 1	grpsubval	⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑌 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
12	6 8 11	syl2anc	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
13	10	subginvcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑆 )
14	13	3adant2	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑆 )
15	9	subgcl	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑆 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ∈ 𝑆 )
16	14 15	syld3an3	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ∈ 𝑆 )
17	12 16	eqeltrd	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) ∈ 𝑆 )