Proof of Theorem mulgnn0dir
| Step | Hyp | Ref
| Expression |
| 1 | | mndsgrp 18753 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) |
| 2 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝐺 ∈ Smgrp) |
| 3 | 2 | ad2antrr 726 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝐺 ∈ Smgrp) |
| 4 | | simplr 769 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℕ) |
| 5 | | simpr 484 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
| 6 | | simpr3 1197 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 7 | 6 | ad2antrr 726 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝐵) |
| 8 | | mulgnndir.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
| 9 | | mulgnndir.t |
. . . . 5
⊢ · =
(.g‘𝐺) |
| 10 | | mulgnndir.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
| 11 | 8, 9, 10 | mulgnndir 19121 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 12 | 3, 4, 5, 7, 11 | syl13anc 1374 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 13 | | simpll 767 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝐺 ∈ Mnd) |
| 14 | | simpr1 1195 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑀 ∈
ℕ0) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈
ℕ0) |
| 16 | | simplr3 1218 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑋 ∈ 𝐵) |
| 17 | 8, 9, 13, 15, 16 | mulgnn0cld 19113 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 · 𝑋) ∈ 𝐵) |
| 18 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 19 | 8, 10, 18 | mndrid 18768 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
| 20 | 13, 17, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
| 21 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑁 = 0) |
| 22 | 21 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0 · 𝑋)) |
| 23 | 8, 18, 9 | mulg0 19092 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
| 24 | 16, 23 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
| 25 | 22, 24 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0g‘𝐺)) |
| 26 | 25 | oveq2d 7447 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((𝑀 · 𝑋) + (0g‘𝐺))) |
| 27 | 21 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = (𝑀 + 0)) |
| 28 | 15 | nn0cnd 12589 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈ ℂ) |
| 29 | 28 | addridd 11461 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 0) = 𝑀) |
| 30 | 27, 29 | eqtrd 2777 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = 𝑀) |
| 31 | 30 | oveq1d 7446 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑀 · 𝑋)) |
| 32 | 20, 26, 31 | 3eqtr4rd 2788 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 33 | 32 | adantlr 715 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 34 | | simpr2 1196 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑁 ∈
ℕ0) |
| 35 | | elnn0 12528 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
| 36 | 34, 35 | sylib 218 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
| 37 | 36 | adantr 480 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
| 38 | 12, 33, 37 | mpjaodan 961 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 39 | | simpll 767 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝐺 ∈ Mnd) |
| 40 | | simplr2 1217 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈
ℕ0) |
| 41 | | simplr3 1218 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑋 ∈ 𝐵) |
| 42 | 8, 9, 39, 40, 41 | mulgnn0cld 19113 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑁 · 𝑋) ∈ 𝐵) |
| 43 | 8, 10, 18 | mndlid 18767 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
| 44 | 39, 42, 43 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) →
((0g‘𝐺)
+ (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
| 45 | | simpr 484 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑀 = 0) |
| 46 | 45 | oveq1d 7446 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0 · 𝑋)) |
| 47 | 41, 23 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
| 48 | 46, 47 | eqtrd 2777 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0g‘𝐺)) |
| 49 | 48 | oveq1d 7446 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((0g‘𝐺) + (𝑁 · 𝑋))) |
| 50 | 45 | oveq1d 7446 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = (0 + 𝑁)) |
| 51 | 40 | nn0cnd 12589 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈ ℂ) |
| 52 | 51 | addlidd 11462 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 + 𝑁) = 𝑁) |
| 53 | 50, 52 | eqtrd 2777 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = 𝑁) |
| 54 | 53 | oveq1d 7446 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
| 55 | 44, 49, 54 | 3eqtr4rd 2788 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 56 | | elnn0 12528 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
| 57 | 14, 56 | sylib 218 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
| 58 | 38, 55, 57 | mpjaodan 961 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |