Step | Hyp | Ref
| Expression |
1 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑛 · 𝑁) = (1 · 𝑁)) |
2 | 1 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 1 → ((𝑛 · 𝑁) · 𝑋) = ((1 · 𝑁) · 𝑋)) |
3 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝑛 · (𝑁 · 𝑋)) = (1 · (𝑁 · 𝑋))) |
4 | 2, 3 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 1 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋)))) |
5 | 4 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 1 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))))) |
6 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑁) = (𝑚 · 𝑁)) |
7 | 6 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((𝑛 · 𝑁) · 𝑋) = ((𝑚 · 𝑁) · 𝑋)) |
8 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · (𝑁 · 𝑋)) = (𝑚 · (𝑁 · 𝑋))) |
9 | 7, 8 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)))) |
10 | 9 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))))) |
11 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑁) = ((𝑚 + 1) · 𝑁)) |
12 | 11 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → ((𝑛 · 𝑁) · 𝑋) = (((𝑚 + 1) · 𝑁) · 𝑋)) |
13 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · (𝑁 · 𝑋)) = ((𝑚 + 1) · (𝑁 · 𝑋))) |
14 | 12, 13 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
15 | 14 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
16 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝑛 · 𝑁) = (𝑀 · 𝑁)) |
17 | 16 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → ((𝑛 · 𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋)) |
18 | | oveq1 6657 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑛 · (𝑁 · 𝑋)) = (𝑀 · (𝑁 · 𝑋))) |
19 | 17, 18 | eqeq12d 2637 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
20 | 19 | imbi2d 330 |
. . . . 5
⊢ (𝑛 = 𝑀 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))) |
21 | | nncn 11028 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
22 | 21 | mulid2d 10058 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1
· 𝑁) = 𝑁) |
23 | 22 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (1 · 𝑁) = 𝑁) |
24 | 23 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((1 · 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
25 | | sgrpmgm 17289 |
. . . . . . . . . 10
⊢ (𝐺 ∈ SGrp → 𝐺 ∈ Mgm) |
26 | 25 | 3anim1i 1248 |
. . . . . . . . 9
⊢ ((𝐺 ∈ SGrp ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) |
27 | | mulgass.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
28 | | mulgass.t |
. . . . . . . . . 10
⊢ · =
(.g‘𝐺) |
29 | 27, 28 | mulgnncl 17556 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
30 | 26, 29 | syl 17 |
. . . . . . . 8
⊢ ((𝐺 ∈ SGrp ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
31 | 30 | 3coml 1272 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (𝑁 · 𝑋) ∈ 𝐵) |
32 | 27, 28 | mulg1 17548 |
. . . . . . 7
⊢ ((𝑁 · 𝑋) ∈ 𝐵 → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
34 | 24, 33 | eqtr4d 2659 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))) |
35 | | oveq1 6657 |
. . . . . . . 8
⊢ (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
36 | | nncn 11028 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 𝑚 ∈ ℂ) |
38 | | 1cnd 10056 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 1 ∈
ℂ) |
39 | | simpr1 1067 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 𝑁 ∈ ℕ) |
40 | 39 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 𝑁 ∈ ℂ) |
41 | 37, 38, 40 | adddird 10065 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → ((𝑚 + 1) · 𝑁) = ((𝑚 · 𝑁) + (1 · 𝑁))) |
42 | 23 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (1 · 𝑁) = 𝑁) |
43 | 42 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → ((𝑚 · 𝑁) + (1 · 𝑁)) = ((𝑚 · 𝑁) + 𝑁)) |
44 | 41, 43 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → ((𝑚 + 1) · 𝑁) = ((𝑚 · 𝑁) + 𝑁)) |
45 | 44 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) + 𝑁) · 𝑋)) |
46 | | simpr3 1069 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 𝐺 ∈ SGrp) |
47 | | nnmulcl 11043 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑚 · 𝑁) ∈ ℕ) |
48 | 47 | 3ad2antr1 1226 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (𝑚 · 𝑁) ∈ ℕ) |
49 | | simpr2 1068 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → 𝑋 ∈ 𝐵) |
50 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
51 | 27, 28, 50 | mulgnndir 17569 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ SGrp ∧ ((𝑚 · 𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
52 | 46, 48, 39, 49, 51 | syl13anc 1328 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
53 | 45, 52 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
54 | 27, 28, 50 | mulgnnp1 17549 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
55 | 31, 54 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
56 | 53, 55 | eqeq12d 2637 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → ((((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)) ↔ (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋)))) |
57 | 35, 56 | syl5ibr 236 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp)) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
58 | 57 | ex 450 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
59 | 58 | a2d 29 |
. . . . 5
⊢ (𝑚 ∈ ℕ → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))) → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
60 | 5, 10, 15, 20, 34, 59 | nnind 11038 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ SGrp) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
61 | 60 | 3expd 1284 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → (𝐺 ∈ SGrp → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
62 | 61 | com4r 94 |
. 2
⊢ (𝐺 ∈ SGrp → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
63 | 62 | 3imp2 1282 |
1
⊢ ((𝐺 ∈ SGrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |