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 𝐻 = ( 𝐺s 𝑆 )
subgmulg.t = ( .g𝐻 )
Assertion subgmulg ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋𝑆 ) → ( 𝑁 · 𝑋 ) = ( 𝑁 𝑋 ) )

Proof

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