| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = 1 → (𝑛 · 𝑁) = (1 · 𝑁)) |
| 2 | 1 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 = 1 → ((𝑛 · 𝑁) · 𝑋) = ((1 · 𝑁) · 𝑋)) |
| 3 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑛 = 1 → (𝑛 · (𝑁 · 𝑋)) = (1 · (𝑁 · 𝑋))) |
| 4 | 2, 3 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = 1 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋)))) |
| 5 | 4 | imbi2d 340 |
. . . . 5
⊢ (𝑛 = 1 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))))) |
| 6 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑁) = (𝑚 · 𝑁)) |
| 7 | 6 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((𝑛 · 𝑁) · 𝑋) = ((𝑚 · 𝑁) · 𝑋)) |
| 8 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · (𝑁 · 𝑋)) = (𝑚 · (𝑁 · 𝑋))) |
| 9 | 7, 8 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)))) |
| 10 | 9 | imbi2d 340 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))))) |
| 11 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑁) = ((𝑚 + 1) · 𝑁)) |
| 12 | 11 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → ((𝑛 · 𝑁) · 𝑋) = (((𝑚 + 1) · 𝑁) · 𝑋)) |
| 13 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · (𝑁 · 𝑋)) = ((𝑚 + 1) · (𝑁 · 𝑋))) |
| 14 | 12, 13 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
| 15 | 14 | imbi2d 340 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
| 16 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝑛 · 𝑁) = (𝑀 · 𝑁)) |
| 17 | 16 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → ((𝑛 · 𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋)) |
| 18 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑛 · (𝑁 · 𝑋)) = (𝑀 · (𝑁 · 𝑋))) |
| 19 | 17, 18 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑛 = 𝑀 → (((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋)) ↔ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 20 | 19 | imbi2d 340 |
. . . . 5
⊢ (𝑛 = 𝑀 → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑛 · 𝑁) · 𝑋) = (𝑛 · (𝑁 · 𝑋))) ↔ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))) |
| 21 | | nncn 12274 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) |
| 22 | 21 | mullidd 11279 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (1
· 𝑁) = 𝑁) |
| 23 | 22 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (1 · 𝑁) = 𝑁) |
| 24 | 23 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((1 · 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
| 25 | | sgrpmgm 18737 |
. . . . . . . . 9
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) |
| 26 | | mulgass.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
| 27 | | mulgass.t |
. . . . . . . . . 10
⊢ · =
(.g‘𝐺) |
| 28 | 26, 27 | mulgnncl 19107 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 29 | 25, 28 | syl3an1 1164 |
. . . . . . . 8
⊢ ((𝐺 ∈ Smgrp ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 30 | 29 | 3coml 1128 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (𝑁 · 𝑋) ∈ 𝐵) |
| 31 | 26, 27 | mulg1 19099 |
. . . . . . 7
⊢ ((𝑁 · 𝑋) ∈ 𝐵 → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
| 32 | 30, 31 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (1 · (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
| 33 | 24, 32 | eqtr4d 2780 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((1 · 𝑁) · 𝑋) = (1 · (𝑁 · 𝑋))) |
| 34 | | oveq1 7438 |
. . . . . . . 8
⊢ (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
| 35 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → 𝑚 ∈ ℂ) |
| 37 | | simpr1 1195 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → 𝑁 ∈ ℕ) |
| 38 | 37 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → 𝑁 ∈ ℂ) |
| 39 | 36, 38 | adddirp1d 11287 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → ((𝑚 + 1) · 𝑁) = ((𝑚 · 𝑁) + 𝑁)) |
| 40 | 39 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) + 𝑁) · 𝑋)) |
| 41 | | simpr3 1197 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → 𝐺 ∈ Smgrp) |
| 42 | | nnmulcl 12290 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑚 · 𝑁) ∈ ℕ) |
| 43 | 42 | 3ad2antr1 1189 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → (𝑚 · 𝑁) ∈ ℕ) |
| 44 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → 𝑋 ∈ 𝐵) |
| 45 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 46 | 26, 27, 45 | mulgnndir 19121 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Smgrp ∧ ((𝑚 · 𝑁) ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
| 47 | 41, 43, 37, 44, 46 | syl13anc 1374 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → (((𝑚 · 𝑁) + 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
| 48 | 40, 47 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → (((𝑚 + 1) · 𝑁) · 𝑋) = (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋))) |
| 49 | 26, 27, 45 | mulgnnp1 19100 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
| 50 | 30, 49 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → ((𝑚 + 1) · (𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋))) |
| 51 | 48, 50 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → ((((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)) ↔ (((𝑚 · 𝑁) · 𝑋)(+g‘𝐺)(𝑁 · 𝑋)) = ((𝑚 · (𝑁 · 𝑋))(+g‘𝐺)(𝑁 · 𝑋)))) |
| 52 | 34, 51 | imbitrrid 246 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ ∧ (𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp)) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋)))) |
| 53 | 52 | ex 412 |
. . . . . 6
⊢ (𝑚 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋)) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
| 54 | 53 | a2d 29 |
. . . . 5
⊢ (𝑚 ∈ ℕ → (((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑚 · 𝑁) · 𝑋) = (𝑚 · (𝑁 · 𝑋))) → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → (((𝑚 + 1) · 𝑁) · 𝑋) = ((𝑚 + 1) · (𝑁 · 𝑋))))) |
| 55 | 5, 10, 15, 20, 33, 54 | nnind 12284 |
. . . 4
⊢ (𝑀 ∈ ℕ → ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵 ∧ 𝐺 ∈ Smgrp) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 56 | 55 | 3expd 1354 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → (𝐺 ∈ Smgrp → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
| 57 | 56 | com4r 94 |
. 2
⊢ (𝐺 ∈ Smgrp → (𝑀 ∈ ℕ → (𝑁 ∈ ℕ → (𝑋 ∈ 𝐵 → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))))) |
| 58 | 57 | 3imp2 1350 |
1
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |