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

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 ‘ 𝐺 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 · 𝑋 ) = ( 𝑁 ∙ 𝑋 ) )