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

Metamath Proof Explorer

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 ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) ∈ 𝑆 )