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