Proof of Theorem mulgnn0ass
| Step | Hyp | Ref
| Expression |
| 1 | | mndsgrp 18753 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) |
| 2 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝐺 ∈ Smgrp) |
| 3 | 2 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 𝐺 ∈ Smgrp) |
| 4 | | simprl 771 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 𝑀 ∈
ℕ) |
| 5 | | simprr 773 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 𝑁 ∈
ℕ) |
| 6 | | simpr3 1197 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 7 | 6 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → 𝑋 ∈ 𝐵) |
| 8 | | mulgass.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
| 9 | | mulgass.t |
. . . . . . 7
⊢ · =
(.g‘𝐺) |
| 10 | 8, 9 | mulgnnass 19127 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 11 | 3, 4, 5, 7, 10 | syl13anc 1374 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 12 | 11 | expr 456 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 ∈ ℕ → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 13 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 14 | 8, 13, 9 | mulg0 19092 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
| 15 | 6, 14 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (0 · 𝑋) = (0g‘𝐺)) |
| 16 | | simpr1 1195 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑀 ∈
ℕ0) |
| 17 | 16 | nn0cnd 12589 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑀 ∈
ℂ) |
| 18 | 17 | mul01d 11460 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 · 0) =
0) |
| 19 | 18 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 · 0) · 𝑋) = (0 · 𝑋)) |
| 20 | 15 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 · (0 · 𝑋)) = (𝑀 ·
(0g‘𝐺))) |
| 21 | 8, 9, 13 | mulgnn0z 19119 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
| 22 | 21 | 3ad2antr1 1189 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
| 23 | 20, 22 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 · (0 · 𝑋)) = (0g‘𝐺)) |
| 24 | 15, 19, 23 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 · 0) · 𝑋) = (𝑀 · (0 · 𝑋))) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 · 0) · 𝑋) = (𝑀 · (0 · 𝑋))) |
| 26 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑀 · 𝑁) = (𝑀 · 0)) |
| 27 | 26 | oveq1d 7446 |
. . . . . 6
⊢ (𝑁 = 0 → ((𝑀 · 𝑁) · 𝑋) = ((𝑀 · 0) · 𝑋)) |
| 28 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑁 = 0 → (𝑁 · 𝑋) = (0 · 𝑋)) |
| 29 | 28 | oveq2d 7447 |
. . . . . 6
⊢ (𝑁 = 0 → (𝑀 · (𝑁 · 𝑋)) = (𝑀 · (0 · 𝑋))) |
| 30 | 27, 29 | eqeq12d 2753 |
. . . . 5
⊢ (𝑁 = 0 → (((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)) ↔ ((𝑀 · 0) · 𝑋) = (𝑀 · (0 · 𝑋)))) |
| 31 | 25, 30 | syl5ibrcom 247 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 = 0 → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 32 | | simpr2 1196 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑁 ∈
ℕ0) |
| 33 | | elnn0 12528 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 34 | 32, 33 | sylib 218 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
| 35 | 34 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
| 36 | 12, 31, 35 | mpjaod 861 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 37 | 36 | ex 412 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ∈ ℕ → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 38 | 32 | nn0cnd 12589 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑁 ∈
ℂ) |
| 39 | 38 | mul02d 11459 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (0
· 𝑁) =
0) |
| 40 | 39 | oveq1d 7446 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((0
· 𝑁) · 𝑋) = (0 · 𝑋)) |
| 41 | 8, 9 | mulgnn0cl 19108 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 42 | 41 | 3adant3r1 1183 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑁 · 𝑋) ∈ 𝐵) |
| 43 | 8, 13, 9 | mulg0 19092 |
. . . . 5
⊢ ((𝑁 · 𝑋) ∈ 𝐵 → (0 · (𝑁 · 𝑋)) = (0g‘𝐺)) |
| 44 | 42, 43 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (0 · (𝑁 · 𝑋)) = (0g‘𝐺)) |
| 45 | 15, 40, 44 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((0
· 𝑁) · 𝑋) = (0 · (𝑁 · 𝑋))) |
| 46 | | oveq1 7438 |
. . . . 5
⊢ (𝑀 = 0 → (𝑀 · 𝑁) = (0 · 𝑁)) |
| 47 | 46 | oveq1d 7446 |
. . . 4
⊢ (𝑀 = 0 → ((𝑀 · 𝑁) · 𝑋) = ((0 · 𝑁) · 𝑋)) |
| 48 | | oveq1 7438 |
. . . 4
⊢ (𝑀 = 0 → (𝑀 · (𝑁 · 𝑋)) = (0 · (𝑁 · 𝑋))) |
| 49 | 47, 48 | eqeq12d 2753 |
. . 3
⊢ (𝑀 = 0 → (((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)) ↔ ((0 · 𝑁) · 𝑋) = (0 · (𝑁 · 𝑋)))) |
| 50 | 45, 49 | syl5ibrcom 247 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 = 0 → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 51 | | elnn0 12528 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 52 | 16, 51 | sylib 218 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
| 53 | 37, 50, 52 | mpjaod 861 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |