Metamath Proof Explorer

Theorem subgsub

Description: The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses subgsubcl.p ⊢ − = ( -g ‘ 𝐺 )
subgsub.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
subgsub.n ⊢ 𝑁 = ( -g ‘ 𝐻 )
Assertion subgsub ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 𝑁 𝑌 ) )

Proof

Step Hyp Ref Expression
1 subgsubcl.p ⊢ − = ( -g ‘ 𝐺 )
2 subgsub.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
3 subgsub.n ⊢ 𝑁 = ( -g ‘ 𝐻 )
4 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
5 2 4 ressplusg ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
6 5 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
7 eqidd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 = 𝑋 )
8 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
9 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
10 2 8 9 subginv ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) = ( ( invg ‘ 𝐻 ) ‘ 𝑌 ) )
11 10 3adant2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) = ( ( invg ‘ 𝐻 ) ‘ 𝑌 ) )
12 6 7 11 oveq123d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑌 ) ) )
13 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
14 13 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
15 14 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
16 simp2 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
17 15 16 sseldd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
18 simp3 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ 𝑆 )
19 15 18 sseldd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ ( Base ‘ 𝐺 ) )
20 13 4 8 1 grpsubval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑌 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
21 17 19 20 syl2anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
22 2 subgbas ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
23 22 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) )
24 16 23 eleqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
25 18 23 eleqtrd ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ∈ ( Base ‘ 𝐻 ) )
26 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
27 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
28 26 27 9 3 grpsubval ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐻 ) ∧ 𝑌 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑋 𝑁 𝑌 ) = ( 𝑋 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑌 ) ) )
29 24 25 28 syl2anc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 𝑁 𝑌 ) = ( 𝑋 ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ 𝑌 ) ) )
30 12 21 29 3eqtr4d ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 𝑁 𝑌 ) )