Theorem mulgnn0ass

Description: Product of group multiples, generalized to NN0 . (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgass.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	mulgass.t	⊢ · = ( .g ‘ 𝐺 )
Assertion	mulgnn0ass	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		mulgass.t	⊢ · = ( .g ‘ 𝐺 )
3		mndsgrp	⊢ ( 𝐺 ∈ Mnd → 𝐺 ∈ Smgrp )
4	3	adantr	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐺 ∈ Smgrp )
5	4	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → 𝐺 ∈ Smgrp )
6		simprl	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → 𝑀 ∈ ℕ )
7		simprr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
8		simpr3	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
9	8	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → 𝑋 ∈ 𝐵 )
10	1 2	mulgnnass	⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
11	5 6 7 9 10	syl13anc	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
12	11	expr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
13		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14	1 13 2	mulg0	⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
15	8 14	syl	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
16		simpr1	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℕ0 )
17	16	nn0cnd	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑀 ∈ ℂ )
18	17	mul01d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · 0 ) = 0 )
19	18	oveq1d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 0 ) · 𝑋 ) = ( 0 · 𝑋 ) )
20	15	oveq2d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · ( 0 · 𝑋 ) ) = ( 𝑀 · ( 0g ‘ 𝐺 ) ) )
21	1 2 13	mulgnn0z	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 · ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
22	21	3ad2antr1	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐺 ) )
23	20 22	eqtrd	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 · ( 0 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
24	15 19 23	3eqtr4d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 0 ) · 𝑋 ) = ( 𝑀 · ( 0 · 𝑋 ) ) )
25	24	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝑀 · 0 ) · 𝑋 ) = ( 𝑀 · ( 0 · 𝑋 ) ) )
26		oveq2	⊢ ( 𝑁 = 0 → ( 𝑀 · 𝑁 ) = ( 𝑀 · 0 ) )
27	26	oveq1d	⊢ ( 𝑁 = 0 → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 0 ) · 𝑋 ) )
28		oveq1	⊢ ( 𝑁 = 0 → ( 𝑁 · 𝑋 ) = ( 0 · 𝑋 ) )
29	28	oveq2d	⊢ ( 𝑁 = 0 → ( 𝑀 · ( 𝑁 · 𝑋 ) ) = ( 𝑀 · ( 0 · 𝑋 ) ) )
30	27 29	eqeq12d	⊢ ( 𝑁 = 0 → ( ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ↔ ( ( 𝑀 · 0 ) · 𝑋 ) = ( 𝑀 · ( 0 · 𝑋 ) ) ) )
31	25 30	syl5ibrcom	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑁 = 0 → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
32		simpr2	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℕ0 )
33		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
34	32 33	sylib	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
35	34	adantr	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
36	12 31 35	mpjaod	⊢ ( ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) ∧ 𝑀 ∈ ℕ ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
37	36	ex	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 ∈ ℕ → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
38	32	nn0cnd	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑁 ∈ ℂ )
39	38	mul02d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 0 · 𝑁 ) = 0 )
40	39	oveq1d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 · 𝑁 ) · 𝑋 ) = ( 0 · 𝑋 ) )
41	1 2	mulgnn0cl	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
42	41	3adant3r1	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
43	1 13 2	mulg0	⊢ ( ( 𝑁 · 𝑋 ) ∈ 𝐵 → ( 0 · ( 𝑁 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
44	42 43	syl	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 0 · ( 𝑁 · 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
45	15 40 44	3eqtr4d	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 · 𝑁 ) · 𝑋 ) = ( 0 · ( 𝑁 · 𝑋 ) ) )
46		oveq1	⊢ ( 𝑀 = 0 → ( 𝑀 · 𝑁 ) = ( 0 · 𝑁 ) )
47	46	oveq1d	⊢ ( 𝑀 = 0 → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( ( 0 · 𝑁 ) · 𝑋 ) )
48		oveq1	⊢ ( 𝑀 = 0 → ( 𝑀 · ( 𝑁 · 𝑋 ) ) = ( 0 · ( 𝑁 · 𝑋 ) ) )
49	47 48	eqeq12d	⊢ ( 𝑀 = 0 → ( ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ↔ ( ( 0 · 𝑁 ) · 𝑋 ) = ( 0 · ( 𝑁 · 𝑋 ) ) ) )
50	45 49	syl5ibrcom	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 = 0 → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
51		elnn0	⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
52	16 51	sylib	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑀 ∈ ℕ ∨ 𝑀 = 0 ) )
53	37 50 52	mpjaod	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )