Metamath Proof Explorer

Theorem mulgnnass

Description: Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014) (Revised by AV, 29-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 mulgass.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgass.t ⊢ · = ( .g ‘ 𝐺 )
3 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 · 𝑁 ) = ( 1 · 𝑁 ) )
4 3 oveq1d ⊢ ( 𝑛 = 1 → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( ( 1 · 𝑁 ) · 𝑋 ) )
5 oveq1 ⊢ ( 𝑛 = 1 → ( 𝑛 · ( 𝑁 · 𝑋 ) ) = ( 1 · ( 𝑁 · 𝑋 ) ) )
6 4 5 eqeq12d ⊢ ( 𝑛 = 1 → ( ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ↔ ( ( 1 · 𝑁 ) · 𝑋 ) = ( 1 · ( 𝑁 · 𝑋 ) ) ) )
7 6 imbi2d ⊢ ( 𝑛 = 1 → ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 1 · 𝑁 ) · 𝑋 ) = ( 1 · ( 𝑁 · 𝑋 ) ) ) ) )
8 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · 𝑁 ) = ( 𝑚 · 𝑁 ) )
9 8 oveq1d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( ( 𝑚 · 𝑁 ) · 𝑋 ) )
10 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · ( 𝑁 · 𝑋 ) ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ↔ ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) ) )
12 11 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) ) ) )
13 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · 𝑁 ) = ( ( 𝑚 + 1 ) · 𝑁 ) )
14 13 oveq1d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) )
15 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 · ( 𝑁 · 𝑋 ) ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) )
16 14 15 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ↔ ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ) )
17 16 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ) ) )
18 oveq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 · 𝑁 ) = ( 𝑀 · 𝑁 ) )
19 18 oveq1d ⊢ ( 𝑛 = 𝑀 → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( ( 𝑀 · 𝑁 ) · 𝑋 ) )
20 oveq1 ⊢ ( 𝑛 = 𝑀 → ( 𝑛 · ( 𝑁 · 𝑋 ) ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )
21 19 20 eqeq12d ⊢ ( 𝑛 = 𝑀 → ( ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ↔ ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
22 21 imbi2d ⊢ ( 𝑛 = 𝑀 → ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑛 · 𝑁 ) · 𝑋 ) = ( 𝑛 · ( 𝑁 · 𝑋 ) ) ) ↔ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) )
23 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
24 23 mullidd ⊢ ( 𝑁 ∈ ℕ → ( 1 · 𝑁 ) = 𝑁 )
25 24 3ad2ant1 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( 1 · 𝑁 ) = 𝑁 )
26 25 oveq1d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 1 · 𝑁 ) · 𝑋 ) = ( 𝑁 · 𝑋 ) )
27 sgrpmgm ⊢ ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm )
28 1 2 mulgnncl ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
29 27 28 syl3an1 ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
30 29 3coml ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( 𝑁 · 𝑋 ) ∈ 𝐵 )
31 1 2 mulg1 ⊢ ( ( 𝑁 · 𝑋 ) ∈ 𝐵 → ( 1 · ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
32 30 31 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( 1 · ( 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
33 26 32 eqtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 1 · 𝑁 ) · 𝑋 ) = ( 1 · ( 𝑁 · 𝑋 ) ) )
34 oveq1 ⊢ ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) → ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) = ( ( 𝑚 · ( 𝑁 · 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
35 nncn ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℂ )
36 35 adantr ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → 𝑚 ∈ ℂ )
37 simpr1 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → 𝑁 ∈ ℕ )
38 37 nncnd ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → 𝑁 ∈ ℂ )
39 36 38 adddirp1d ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( 𝑚 + 1 ) · 𝑁 ) = ( ( 𝑚 · 𝑁 ) + 𝑁 ) )
40 39 oveq1d ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( ( 𝑚 · 𝑁 ) + 𝑁 ) · 𝑋 ) )
41 simpr3 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → 𝐺 ∈ Smgrp )
42 nnmulcl ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑚 · 𝑁 ) ∈ ℕ )
43 42 3ad2antr1 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( 𝑚 · 𝑁 ) ∈ ℕ )
44 simpr2 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → 𝑋 ∈ 𝐵 )
45 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
46 1 2 45 mulgnndir ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( ( 𝑚 · 𝑁 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( 𝑚 · 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
47 41 43 37 44 46 syl13anc ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( ( 𝑚 · 𝑁 ) + 𝑁 ) · 𝑋 ) = ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
48 40 47 eqtrd ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
49 1 2 45 mulgnnp1 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) = ( ( 𝑚 · ( 𝑁 · 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
50 30 49 sylan2 ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) = ( ( 𝑚 · ( 𝑁 · 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) )
51 48 50 eqeq12d ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ↔ ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) = ( ( 𝑚 · ( 𝑁 · 𝑋 ) ) ( +g ‘ 𝐺 ) ( 𝑁 · 𝑋 ) ) ) )
52 34 51 imbitrrid ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) ) → ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ) )
53 52 ex ⊢ ( 𝑚 ∈ ℕ → ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ) ) )
54 53 a2d ⊢ ( 𝑚 ∈ ℕ → ( ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑚 · 𝑁 ) · 𝑋 ) = ( 𝑚 · ( 𝑁 · 𝑋 ) ) ) → ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( ( 𝑚 + 1 ) · 𝑁 ) · 𝑋 ) = ( ( 𝑚 + 1 ) · ( 𝑁 · 𝑋 ) ) ) ) )
55 7 12 17 22 33 54 nnind ⊢ ( 𝑀 ∈ ℕ → ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) )
56 55 3expd ⊢ ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐵 → ( 𝐺 ∈ Smgrp → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) ) )
57 56 com4r ⊢ ( 𝐺 ∈ Smgrp → ( 𝑀 ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝑋 ∈ 𝐵 → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) ) ) ) )
58 57 3imp2 ⊢ ( ( 𝐺 ∈ Smgrp ∧ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑀 · 𝑁 ) · 𝑋 ) = ( 𝑀 · ( 𝑁 · 𝑋 ) ) )