Metamath Proof Explorer

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