Metamath Proof Explorer

Theorem submmulg

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

Ref Expression
Hypotheses submmulgcl.t ⊢ ∙ = ( .g ‘ 𝐺 )
submmulg.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
submmulg.t ⊢ · = ( .g ‘ 𝐻 )
Assertion submmulg ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∙ 𝑋 ) = ( 𝑁 · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 submmulgcl.t ⊢ ∙ = ( .g ‘ 𝐺 )
2 submmulg.h ⊢ 𝐻 = ( 𝐺 ↾s 𝑆 )
3 submmulg.t ⊢ · = ( .g ‘ 𝐻 )
4 simpl1 ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
5 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6 2 5 ressplusg ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
7 4 6 syl ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) )
8 7 seqeq2d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) )
9 8 fveq1d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
10 simpr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 11 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
13 12 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) )
14 simp3 ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
15 13 14 sseldd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
17 eqid ⊢ seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) )
18 11 5 1 17 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑁 ∙ 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
19 10 16 18 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∙ 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐺 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
20 2 submbas ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) )
21 20 3ad2ant1 ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 = ( Base ‘ 𝐻 ) )
22 14 21 eleqtrd ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
23 22 adantr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
24 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
25 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
26 eqid ⊢ seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) = seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) )
27 24 25 3 26 mulgnn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
28 10 23 27 syl2anc ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 · 𝑋 ) = ( seq 1 ( ( +g ‘ 𝐻 ) , ( ℕ × { 𝑋 } ) ) ‘ 𝑁 ) )
29 9 19 28 3eqtr4d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 ∙ 𝑋 ) = ( 𝑁 · 𝑋 ) )
30 simpl1 ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 𝑆 ∈ ( SubMnd ‘ 𝐺 ) )
31 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
32 2 31 subm0 ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
33 30 32 syl ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) )
34 15 adantr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
35 11 31 1 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → ( 0 ∙ 𝑋 ) = ( 0g ‘ 𝐺 ) )
36 34 35 syl ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 0 ∙ 𝑋 ) = ( 0g ‘ 𝐺 ) )
37 22 adantr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 𝑋 ∈ ( Base ‘ 𝐻 ) )
38 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
39 24 38 3 mulg0 ⊢ ( 𝑋 ∈ ( Base ‘ 𝐻 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐻 ) )
40 37 39 syl ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐻 ) )
41 33 36 40 3eqtr4d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 0 ∙ 𝑋 ) = ( 0 · 𝑋 ) )
42 simpr ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → 𝑁 = 0 )
43 42 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 ∙ 𝑋 ) = ( 0 ∙ 𝑋 ) )
44 42 oveq1d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
45 41 43 44 3eqtr4d ⊢ ( ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) ∧ 𝑁 = 0 ) → ( 𝑁 ∙ 𝑋 ) = ( 𝑁 · 𝑋 ) )
46 simp2 ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → 𝑁 ∈ ℕ0 )
47 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
48 46 47 sylib ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
49 29 45 48 mpjaodan ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑁 ∙ 𝑋 ) = ( 𝑁 · 𝑋 ) )