Proof of Theorem mulgnn0dir
Step | Hyp | Ref
| Expression |
1 | | mndsgrp 18562 |
. . . . . 6
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp) |
2 | 1 | adantr 481 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝐺 ∈ Smgrp) |
3 | 2 | ad2antrr 724 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝐺 ∈ Smgrp) |
4 | | simplr 767 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑀 ∈
ℕ) |
5 | | simpr 485 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℕ) |
6 | | simpr3 1196 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑋 ∈ 𝐵) |
7 | 6 | ad2antrr 724 |
. . . 4
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → 𝑋 ∈ 𝐵) |
8 | | mulgnndir.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
9 | | mulgnndir.t |
. . . . 5
⊢ · =
(.g‘𝐺) |
10 | | mulgnndir.p |
. . . . 5
⊢ + =
(+g‘𝐺) |
11 | 8, 9, 10 | mulgnndir 18905 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
12 | 3, 4, 5, 7, 11 | syl13anc 1372 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
13 | | simpll 765 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝐺 ∈ Mnd) |
14 | | simpr1 1194 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑀 ∈
ℕ0) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈
ℕ0) |
16 | | simplr3 1217 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑋 ∈ 𝐵) |
17 | 8, 9, 13, 15, 16 | mulgnn0cld 18897 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 · 𝑋) ∈ 𝐵) |
18 | | eqid 2736 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
19 | 8, 10, 18 | mndrid 18577 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
20 | 13, 17, 19 | syl2anc 584 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (0g‘𝐺)) = (𝑀 · 𝑋)) |
21 | | simpr 485 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑁 = 0) |
22 | 21 | oveq1d 7372 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0 · 𝑋)) |
23 | 8, 18, 9 | mulg0 18879 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
24 | 16, 23 | syl 17 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
25 | 22, 24 | eqtrd 2776 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑁 · 𝑋) = (0g‘𝐺)) |
26 | 25 | oveq2d 7373 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((𝑀 · 𝑋) + (0g‘𝐺))) |
27 | 21 | oveq2d 7373 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = (𝑀 + 0)) |
28 | 15 | nn0cnd 12475 |
. . . . . . . 8
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → 𝑀 ∈ ℂ) |
29 | 28 | addid1d 11355 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 0) = 𝑀) |
30 | 27, 29 | eqtrd 2776 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → (𝑀 + 𝑁) = 𝑀) |
31 | 30 | oveq1d 7372 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑀 · 𝑋)) |
32 | 20, 26, 31 | 3eqtr4rd 2787 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
33 | 32 | adantlr 713 |
. . 3
⊢ ((((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) ∧ 𝑁 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
34 | | simpr2 1195 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → 𝑁 ∈
ℕ0) |
35 | | elnn0 12415 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
36 | 34, 35 | sylib 217 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
37 | 36 | adantr 481 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → (𝑁 ∈ ℕ ∨ 𝑁 = 0)) |
38 | 12, 33, 37 | mpjaodan 957 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 ∈ ℕ) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
39 | | simpll 765 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝐺 ∈ Mnd) |
40 | | simplr2 1216 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈
ℕ0) |
41 | | simplr3 1217 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑋 ∈ 𝐵) |
42 | 8, 9, 39, 40, 41 | mulgnn0cld 18897 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑁 · 𝑋) ∈ 𝐵) |
43 | 8, 10, 18 | mndlid 18576 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((0g‘𝐺) + (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
44 | 39, 42, 43 | syl2anc 584 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) →
((0g‘𝐺)
+ (𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
45 | | simpr 485 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑀 = 0) |
46 | 45 | oveq1d 7372 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0 · 𝑋)) |
47 | 41, 23 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 · 𝑋) = (0g‘𝐺)) |
48 | 46, 47 | eqtrd 2776 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 · 𝑋) = (0g‘𝐺)) |
49 | 48 | oveq1d 7372 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((0g‘𝐺) + (𝑁 · 𝑋))) |
50 | 45 | oveq1d 7372 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = (0 + 𝑁)) |
51 | 40 | nn0cnd 12475 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → 𝑁 ∈ ℂ) |
52 | 51 | addid2d 11356 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (0 + 𝑁) = 𝑁) |
53 | 50, 52 | eqtrd 2776 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → (𝑀 + 𝑁) = 𝑁) |
54 | 53 | oveq1d 7372 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = (𝑁 · 𝑋)) |
55 | 44, 49, 54 | 3eqtr4rd 2787 |
. 2
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) ∧ 𝑀 = 0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
56 | | elnn0 12415 |
. . 3
⊢ (𝑀 ∈ ℕ0
↔ (𝑀 ∈ ℕ
∨ 𝑀 =
0)) |
57 | 14, 56 | sylib 217 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → (𝑀 ∈ ℕ ∨ 𝑀 = 0)) |
58 | 38, 55, 57 | mpjaodan 957 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |