Proof of Theorem mulgdirlem
| Step | Hyp | Ref
| Expression |
| 1 | | simpl1 1192 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → 𝐺 ∈ Grp) |
| 2 | 1 | grpmndd 18964 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → 𝐺 ∈ Mnd) |
| 3 | | simprl 771 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → 𝑀 ∈
ℕ0) |
| 4 | | simprr 773 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → 𝑁 ∈
ℕ0) |
| 5 | | simpl23 1254 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → 𝑋 ∈ 𝐵) |
| 6 | | mulgnndir.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 7 | | mulgnndir.t |
. . . . . 6
⊢ · =
(.g‘𝐺) |
| 8 | | mulgnndir.p |
. . . . . 6
⊢ + =
(+g‘𝐺) |
| 9 | 6, 7, 8 | mulgnn0dir 19122 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 10 | 2, 3, 4, 5, 9 | syl13anc 1374 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 11 | 10 | anassrs 467 |
. . 3
⊢ ((((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0)
∧ 𝑁 ∈
ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 12 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝐺 ∈ Grp) |
| 13 | | simp22 1208 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈
ℤ) |
| 14 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝑁 ∈ ℤ) |
| 15 | | simpl23 1254 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝑋 ∈ 𝐵) |
| 16 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 17 | 6, 7, 16 | mulgneg 19110 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
| 18 | 12, 14, 15, 17 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
| 19 | 18 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((-𝑁 · 𝑋) + (𝑁 · 𝑋)) = (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋))) |
| 20 | 6, 7 | mulgcl 19109 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 21 | 12, 14, 15, 20 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (𝑁 · 𝑋) ∈ 𝐵) |
| 22 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 23 | 6, 8, 22, 16 | grplinv 19007 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑋) ∈ 𝐵) → (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (0g‘𝐺)) |
| 24 | 12, 21, 23 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (0g‘𝐺)) |
| 25 | 19, 24 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((-𝑁 · 𝑋) + (𝑁 · 𝑋)) = (0g‘𝐺)) |
| 26 | 25 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺))) |
| 27 | | simpl3 1194 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (𝑀 + 𝑁) ∈
ℕ0) |
| 28 | | nn0z 12638 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) ∈ ℕ0 → (𝑀 + 𝑁) ∈ ℤ) |
| 29 | 27, 28 | syl 17 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (𝑀 + 𝑁) ∈ ℤ) |
| 30 | 6, 7 | mulgcl 19109 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) |
| 31 | 12, 29, 15, 30 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) |
| 32 | 6, 8, 22 | grprid 18986 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) → (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺)) = ((𝑀 + 𝑁) · 𝑋)) |
| 33 | 12, 31, 32 | syl2anc 584 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺)) = ((𝑀 + 𝑁) · 𝑋)) |
| 34 | 26, 33 | eqtrd 2777 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = ((𝑀 + 𝑁) · 𝑋)) |
| 35 | | nn0z 12638 |
. . . . . . . . 9
⊢ (-𝑁 ∈ ℕ0
→ -𝑁 ∈
ℤ) |
| 36 | 35 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → -𝑁 ∈ ℤ) |
| 37 | 6, 7 | mulgcl 19109 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) ∈ 𝐵) |
| 38 | 12, 36, 15, 37 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (-𝑁 · 𝑋) ∈ 𝐵) |
| 39 | 6, 8 | grpass 18960 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (((𝑀 + 𝑁) · 𝑋) ∈ 𝐵 ∧ (-𝑁 · 𝑋) ∈ 𝐵 ∧ (𝑁 · 𝑋) ∈ 𝐵)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋)))) |
| 40 | 12, 31, 38, 21, 39 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋)))) |
| 41 | 12 | grpmndd 18964 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝐺 ∈ Mnd) |
| 42 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → -𝑁 ∈
ℕ0) |
| 43 | 6, 7, 8 | mulgnn0dir 19122 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Mnd ∧ ((𝑀 + 𝑁) ∈ ℕ0 ∧ -𝑁 ∈ ℕ0
∧ 𝑋 ∈ 𝐵)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋))) |
| 44 | 41, 27, 42, 15, 43 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋))) |
| 45 | | simp21 1207 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈
ℤ) |
| 46 | 45 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈
ℂ) |
| 47 | 13 | zcnd 12723 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈
ℂ) |
| 48 | 46, 47 | addcld 11280 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℂ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (𝑀 + 𝑁) ∈ ℂ) |
| 50 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝑁 ∈ ℂ) |
| 51 | 49, 50 | negsubd 11626 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) + -𝑁) = ((𝑀 + 𝑁) − 𝑁)) |
| 52 | 46 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → 𝑀 ∈ ℂ) |
| 53 | 52, 50 | pncand 11621 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) − 𝑁) = 𝑀) |
| 54 | 51, 53 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) + -𝑁) = 𝑀) |
| 55 | 54 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (𝑀 · 𝑋)) |
| 56 | 44, 55 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) = (𝑀 · 𝑋)) |
| 57 | 56 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 58 | 40, 57 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 59 | 34, 58 | eqtr3d 2779 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 60 | 59 | anassrs 467 |
. . 3
⊢ ((((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0)
∧ -𝑁 ∈
ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 61 | | elznn0 12628 |
. . . . . 6
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
| 62 | 61 | simprbi 496 |
. . . . 5
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0)) |
| 63 | 13, 62 | syl 17 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0)) |
| 64 | 63 | adantr 480 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0)
→ (𝑁 ∈
ℕ0 ∨ -𝑁
∈ ℕ0)) |
| 65 | 11, 60, 64 | mpjaodan 961 |
. 2
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0)
→ ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 66 | | simpl1 1192 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝐺 ∈
Grp) |
| 67 | 45 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℤ) |
| 68 | | simpl23 1254 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝑋 ∈ 𝐵) |
| 69 | 6, 7 | mulgcl 19109 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) ∈ 𝐵) |
| 70 | 66, 67, 68, 69 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (𝑀 · 𝑋) ∈ 𝐵) |
| 71 | 67 | znegcld 12724 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ -𝑀 ∈
ℤ) |
| 72 | 6, 7 | mulgcl 19109 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ -𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑀 · 𝑋) ∈ 𝐵) |
| 73 | 66, 71, 68, 72 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (-𝑀 · 𝑋) ∈ 𝐵) |
| 74 | 28 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℤ) |
| 75 | 74 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (𝑀 + 𝑁) ∈
ℤ) |
| 76 | 66, 75, 68, 30 | syl3anc 1373 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) |
| 77 | 6, 8 | grpass 18960 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 · 𝑋) ∈ 𝐵 ∧ (-𝑀 · 𝑋) ∈ 𝐵 ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵)) → (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)))) |
| 78 | 66, 70, 73, 76, 77 | syl13anc 1374 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)))) |
| 79 | 6, 7, 16 | mulgneg 19110 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑀 · 𝑋) = ((invg‘𝐺)‘(𝑀 · 𝑋))) |
| 80 | 66, 67, 68, 79 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (-𝑀 · 𝑋) =
((invg‘𝐺)‘(𝑀 · 𝑋))) |
| 81 | 80 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 · 𝑋) + (-𝑀 · 𝑋)) = ((𝑀 · 𝑋) +
((invg‘𝐺)‘(𝑀 · 𝑋)))) |
| 82 | 6, 8, 22, 16 | grprinv 19008 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) +
((invg‘𝐺)‘(𝑀 · 𝑋))) = (0g‘𝐺)) |
| 83 | 66, 70, 82 | syl2anc 584 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 · 𝑋) +
((invg‘𝐺)‘(𝑀 · 𝑋))) = (0g‘𝐺)) |
| 84 | 81, 83 | eqtrd 2777 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 · 𝑋) + (-𝑀 · 𝑋)) = (0g‘𝐺)) |
| 85 | 84 | oveq1d 7446 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋))) |
| 86 | 6, 8, 22 | grplid 18985 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) → ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋)) |
| 87 | 66, 76, 86 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋)) |
| 88 | 85, 87 | eqtrd 2777 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋)) |
| 89 | 66 | grpmndd 18964 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝐺 ∈
Mnd) |
| 90 | | simpr 484 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ -𝑀 ∈
ℕ0) |
| 91 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (𝑀 + 𝑁) ∈
ℕ0) |
| 92 | 6, 7, 8 | mulgnn0dir 19122 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0
∧ (𝑀 + 𝑁) ∈ ℕ0
∧ 𝑋 ∈ 𝐵)) → ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))) |
| 93 | 89, 90, 91, 68, 92 | syl13anc 1374 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))) |
| 94 | 46 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℂ) |
| 95 | 94 | negcld 11607 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ -𝑀 ∈
ℂ) |
| 96 | 48 | adantr 480 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (𝑀 + 𝑁) ∈
ℂ) |
| 97 | 95, 96 | addcomd 11463 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (-𝑀 + (𝑀 + 𝑁)) = ((𝑀 + 𝑁) + -𝑀)) |
| 98 | 96, 94 | negsubd 11626 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 + 𝑁) + -𝑀) = ((𝑀 + 𝑁) − 𝑀)) |
| 99 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℂ) |
| 100 | 94, 99 | pncan2d 11622 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 + 𝑁) − 𝑀) = 𝑁) |
| 101 | 97, 98, 100 | 3eqtrd 2781 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ (-𝑀 + (𝑀 + 𝑁)) = 𝑁) |
| 102 | 101 | oveq1d 7446 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = (𝑁 · 𝑋)) |
| 103 | 93, 102 | eqtr3d 2779 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)) = (𝑁 · 𝑋)) |
| 104 | 103 | oveq2d 7447 |
. . 3
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 105 | 78, 88, 104 | 3eqtr3d 2785 |
. 2
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0)
→ ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |
| 106 | | elznn0 12628 |
. . . 4
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0))) |
| 107 | 106 | simprbi 496 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0)) |
| 108 | 45, 107 | syl 17 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0)) |
| 109 | 65, 105, 108 | mpjaodan 961 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |