Proof of Theorem mulgnn0dir
Step | Hyp | Ref
| Expression |
1 | | mndsgrp 17299 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ SGrp) |
2 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝐺 ∈ SGrp) |
3 | 2 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → 𝐺 ∈ SGrp) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝐺 ∈ SGrp) |
5 | | simplr 792 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℕ) |
6 | | simpr 477 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
7 | | simpr3 1069 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑋 ∈ 𝐵) |
8 | 7 | ad2antrr 762 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝐵) |
9 | | mulgnndir.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
10 | | mulgnndir.t |
. . . . 5
⊢ · =
(.g‘𝐺) |
11 | | mulgnndir.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
12 | 9, 10, 11 | mulgnndir 17569 |
. . . 4
⊢ ((𝐺 ∈ SGrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
13 | 4, 5, 6, 8, 12 | syl13anc 1328 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
14 | | simpll 790 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝐺 ∈ Mnd) |
15 | | simpr1 1067 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑀 ∈
ℕ0) |
16 | 15 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈
ℕ0) |
17 | | simplr3 1105 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑋 ∈ 𝐵) |
18 | 9, 10 | mulgnn0cl 17558 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) ∈ 𝐵) |
19 | 14, 16, 17, 18 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 · 𝑋) ∈ 𝐵) |
20 | | eqid 2622 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
21 | 9, 11, 20 | mndrid 17312 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
22 | 14, 19, 21 | syl2anc 693 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
23 | | simpr 477 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑁 = 0) |
24 | 23 | oveq1d 6665 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0 · 𝑋)) |
25 | 9, 20, 10 | mulg0 17546 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
26 | 17, 25 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
27 | 24, 26 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0g‘𝐺)) |
28 | 27 | oveq2d 6666 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((𝑀 · 𝑋) + (0g‘𝐺))) |
29 | 23 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = (𝑀 + 0)) |
30 | 16 | nn0cnd 11353 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈ ℂ) |
31 | 30 | addid1d 10236 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 0) = 𝑀) |
32 | 29, 31 | eqtrd 2656 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = 𝑀) |
33 | 32 | oveq1d 6665 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑀 · 𝑋)) |
34 | 22, 28, 33 | 3eqtr4rd 2667 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
35 | 34 | adantlr 751 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
36 | | simpr2 1068 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑁 ∈
ℕ0) |
37 | | elnn0 11294 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
38 | 36, 37 | sylib 208 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
39 | 38 | adantr 481 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
40 | 13, 35, 39 | mpjaodan 827 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
41 | | simpll 790 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝐺 ∈ Mnd) |
42 | | simplr2 1104 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈
ℕ0) |
43 | | simplr3 1105 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑋 ∈ 𝐵) |
44 | 9, 10 | mulgnn0cl 17558 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
45 | 41, 42, 43, 44 | syl3anc 1326 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑁 · 𝑋) ∈ 𝐵) |
46 | 9, 11, 20 | mndlid 17311 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
47 | 41, 45, 46 | syl2anc 693 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) →
((0g‘𝐺)
+ (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
48 | | simpr 477 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑀 = 0) |
49 | 48 | oveq1d 6665 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0 · 𝑋)) |
50 | 43, 25 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
51 | 49, 50 | eqtrd 2656 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0g‘𝐺)) |
52 | 51 | oveq1d 6665 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((0g‘𝐺) + (𝑁 · 𝑋))) |
53 | 48 | oveq1d 6665 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = (0 + 𝑁)) |
54 | 42 | nn0cnd 11353 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈ ℂ) |
55 | 54 | addid2d 10237 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 + 𝑁) = 𝑁) |
56 | 53, 55 | eqtrd 2656 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = 𝑁) |
57 | 56 | oveq1d 6665 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
58 | 47, 52, 57 | 3eqtr4rd 2667 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
59 | | elnn0 11294 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
60 | 15, 59 | sylib 208 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
61 | 40, 58, 60 | mpjaodan 827 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |