Metamath Proof Explorer

Theorem subgmulg

Description: A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses subgmulgcl.t ⊢ · ˙ = ⋅ G
subgmulg.h ⊢ H = G ↾ 𝑠 S
subgmulg.t ⊢ ∙ ˙ = ⋅ H
Assertion subgmulg ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N · ˙ X = N ∙ ˙ X

Proof

Step Hyp Ref Expression
1 subgmulgcl.t ⊢ · ˙ = ⋅ G
2 subgmulg.h ⊢ H = G ↾ 𝑠 S
3 subgmulg.t ⊢ ∙ ˙ = ⋅ H
4 eqid ⊢ 0 G = 0 G
5 2 4 subg0 ⊢ S ∈ SubGrp ⁡ G → 0 G = 0 H
6 5 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → 0 G = 0 H
7 6 ifeq1d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → if N = 0 0 G if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if N = 0 0 H if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N
8 eqid ⊢ + G = + G
9 2 8 ressplusg ⊢ S ∈ SubGrp ⁡ G → + G = + H
10 9 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → + G = + H
11 10 seqeq2d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → seq 1 + G ℕ × X = seq 1 + H ℕ × X
12 11 adantr ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 → seq 1 + G ℕ × X = seq 1 + H ℕ × X
13 12 fveq1d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 → seq 1 + G ℕ × X ⁡ N = seq 1 + H ℕ × X ⁡ N
14 13 ifeq1d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 → if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N
15 simp2 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N ∈ ℤ
16 15 zred ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N ∈ ℝ
17 0re ⊢ 0 ∈ ℝ
18 axlttri ⊢ N ∈ ℝ ∧ 0 ∈ ℝ → N < 0 ↔ ¬ N = 0 ∨ 0 < N
19 16 17 18 sylancl ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N < 0 ↔ ¬ N = 0 ∨ 0 < N
20 ioran ⊢ ¬ N = 0 ∨ 0 < N ↔ ¬ N = 0 ∧ ¬ 0 < N
21 19 20 bitrdi ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N < 0 ↔ ¬ N = 0 ∧ ¬ 0 < N
22 21 biimpar ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → N < 0
23 simpl1 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → S ∈ SubGrp ⁡ G
24 15 adantr ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → N ∈ ℤ
25 24 znegcld ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → − N ∈ ℤ
26 16 lt0neg1d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N < 0 ↔ 0 < − N
27 26 biimpa ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → 0 < − N
28 elnnz ⊢ − N ∈ ℕ ↔ − N ∈ ℤ ∧ 0 < − N
29 25 27 28 sylanbrc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → − N ∈ ℕ
30 eqid ⊢ Base G = Base G
31 30 subgss ⊢ S ∈ SubGrp ⁡ G → S ⊆ Base G
32 31 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → S ⊆ Base G
33 simp3 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → X ∈ S
34 32 33 sseldd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → X ∈ Base G
35 34 adantr ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → X ∈ Base G
36 eqid ⊢ seq 1 + G ℕ × X = seq 1 + G ℕ × X
37 30 8 1 36 mulgnn ⊢ − N ∈ ℕ ∧ X ∈ Base G → -N · ˙ X = seq 1 + G ℕ × X ⁡ − N
38 29 35 37 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → -N · ˙ X = seq 1 + G ℕ × X ⁡ − N
39 33 adantr ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → X ∈ S
40 1 subgmulgcl ⊢ S ∈ SubGrp ⁡ G ∧ − N ∈ ℤ ∧ X ∈ S → -N · ˙ X ∈ S
41 23 25 39 40 syl3anc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → -N · ˙ X ∈ S
42 38 41 eqeltrrd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → seq 1 + G ℕ × X ⁡ − N ∈ S
43 eqid ⊢ inv g ⁡ G = inv g ⁡ G
44 eqid ⊢ inv g ⁡ H = inv g ⁡ H
45 2 43 44 subginv ⊢ S ∈ SubGrp ⁡ G ∧ seq 1 + G ℕ × X ⁡ − N ∈ S → inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + G ℕ × X ⁡ − N
46 23 42 45 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ N < 0 → inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + G ℕ × X ⁡ − N
47 22 46 syldan ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + G ℕ × X ⁡ − N
48 11 adantr ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → seq 1 + G ℕ × X = seq 1 + H ℕ × X
49 48 fveq1d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → seq 1 + G ℕ × X ⁡ − N = seq 1 + H ℕ × X ⁡ − N
50 49 fveq2d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → inv g ⁡ H ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
51 47 50 eqtrd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
52 51 anassrs ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 ∧ ¬ 0 < N → inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
53 52 ifeq2da ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 → if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
54 14 53 eqtrd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S ∧ ¬ N = 0 → if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
55 54 ifeq2da ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → if N = 0 0 H if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if N = 0 0 H if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
56 7 55 eqtrd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → if N = 0 0 G if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N = if N = 0 0 H if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
57 30 8 4 43 1 36 mulgval ⊢ N ∈ ℤ ∧ X ∈ Base G → N · ˙ X = if N = 0 0 G if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N
58 15 34 57 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N · ˙ X = if N = 0 0 G if 0 < N seq 1 + G ℕ × X ⁡ N inv g ⁡ G ⁡ seq 1 + G ℕ × X ⁡ − N
59 2 subgbas ⊢ S ∈ SubGrp ⁡ G → S = Base H
60 59 3ad2ant1 ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → S = Base H
61 33 60 eleqtrd ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → X ∈ Base H
62 eqid ⊢ Base H = Base H
63 eqid ⊢ + H = + H
64 eqid ⊢ 0 H = 0 H
65 eqid ⊢ seq 1 + H ℕ × X = seq 1 + H ℕ × X
66 62 63 64 44 3 65 mulgval ⊢ N ∈ ℤ ∧ X ∈ Base H → N ∙ ˙ X = if N = 0 0 H if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
67 15 61 66 syl2anc ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N ∙ ˙ X = if N = 0 0 H if 0 < N seq 1 + H ℕ × X ⁡ N inv g ⁡ H ⁡ seq 1 + H ℕ × X ⁡ − N
68 56 58 67 3eqtr4d ⊢ S ∈ SubGrp ⁡ G ∧ N ∈ ℤ ∧ X ∈ S → N · ˙ X = N ∙ ˙ X