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 ⊢ H = G ↾ 𝑠 S
subgsub.n ⊢ N = - H
Assertion subgsub ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X - ˙ Y = X N Y

Proof

Step Hyp Ref Expression
1 subgsubcl.p ⊢ - ˙ = - G
2 subgsub.h ⊢ H = G ↾ 𝑠 S
3 subgsub.n ⊢ N = - H
4 eqid ⊢ + G = + G
5 2 4 ressplusg ⊢ S ∈ SubGrp ⁡ G → + G = + H
6 5 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → + G = + H
7 eqidd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X = X
8 eqid ⊢ inv g ⁡ G = inv g ⁡ G
9 eqid ⊢ inv g ⁡ H = inv g ⁡ H
10 2 8 9 subginv ⊢ S ∈ SubGrp ⁡ G ∧ Y ∈ S → inv g ⁡ G ⁡ Y = inv g ⁡ H ⁡ Y
11 10 3adant2 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → inv g ⁡ G ⁡ Y = inv g ⁡ H ⁡ Y
12 6 7 11 oveq123d ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X + G inv g ⁡ G ⁡ Y = X + H inv g ⁡ H ⁡ Y
13 eqid ⊢ Base G = Base G
14 13 subgss ⊢ S ∈ SubGrp ⁡ G → S ⊆ Base G
15 14 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → S ⊆ Base G
16 simp2 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X ∈ S
17 15 16 sseldd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X ∈ Base G
18 simp3 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → Y ∈ S
19 15 18 sseldd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → Y ∈ Base G
20 13 4 8 1 grpsubval ⊢ X ∈ Base G ∧ Y ∈ Base G → X - ˙ Y = X + G inv g ⁡ G ⁡ Y
21 17 19 20 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X - ˙ Y = X + G inv g ⁡ G ⁡ Y
22 2 subgbas ⊢ S ∈ SubGrp ⁡ G → S = Base H
23 22 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → S = Base H
24 16 23 eleqtrd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X ∈ Base H
25 18 23 eleqtrd ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → Y ∈ Base H
26 eqid ⊢ Base H = Base H
27 eqid ⊢ + H = + H
28 26 27 9 3 grpsubval ⊢ X ∈ Base H ∧ Y ∈ Base H → X N Y = X + H inv g ⁡ H ⁡ Y
29 24 25 28 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X N Y = X + H inv g ⁡ H ⁡ Y
30 12 21 29 3eqtr4d ⊢ S ∈ SubGrp ⁡ G ∧ X ∈ S ∧ Y ∈ S → X - ˙ Y = X N Y