Proof of Theorem mulgass
| Step | Hyp | Ref
| Expression |
| 1 | | simpr1 1195 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ) |
| 2 | | elznn0 12628 |
. . . 4
⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0))) |
| 3 | 2 | simprbi 496 |
. . 3
⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℕ0 ∨
-𝑀 ∈
ℕ0)) |
| 4 | 1, 3 | syl 17 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 ∈ ℕ0 ∨ -𝑀 ∈
ℕ0)) |
| 5 | | simpr2 1196 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℤ) |
| 6 | | elznn0 12628 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
| 7 | 6 | simprbi 496 |
. . 3
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0)) |
| 8 | 5, 7 | syl 17 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0)) |
| 9 | | grpmnd 18958 |
. . . . . 6
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
| 10 | 9 | ad2antrr 726 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝐺 ∈
Mnd) |
| 11 | | simprl 771 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝑀 ∈
ℕ0) |
| 12 | | simprr 773 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝑁 ∈
ℕ0) |
| 13 | | simplr3 1218 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝑋 ∈ 𝐵) |
| 14 | | mulgass.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
| 15 | | mulgass.t |
. . . . . 6
⊢ · =
(.g‘𝐺) |
| 16 | 14, 15 | mulgnn0ass 19128 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 17 | 10, 11, 12, 13, 16 | syl13anc 1374 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 18 | 17 | ex 412 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 19 | 1 | zcnd 12723 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℂ) |
| 20 | 5 | zcnd 12723 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℂ) |
| 21 | 19, 20 | mulneg1d 11716 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
| 22 | 21 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ (-𝑀 · 𝑁) = -(𝑀 · 𝑁)) |
| 23 | 22 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((-𝑀 · 𝑁) · 𝑋) = (-(𝑀 · 𝑁) · 𝑋)) |
| 24 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝐺 ∈
Mnd) |
| 25 | | simprl 771 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ -𝑀 ∈
ℕ0) |
| 26 | | simprr 773 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝑁 ∈
ℕ0) |
| 27 | | simpr3 1197 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 28 | 27 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ 𝑋 ∈ 𝐵) |
| 29 | 14, 15 | mulgnn0ass 19128 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((-𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) |
| 30 | 24, 25, 26, 28, 29 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((-𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) |
| 31 | 23, 30 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) |
| 32 | | fveq2 6906 |
. . . . . . 7
⊢ ((-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋)))) |
| 33 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝐺 ∈ Grp) |
| 34 | 1, 5 | zmulcld 12728 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · 𝑁) ∈ ℤ) |
| 35 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 36 | 14, 15, 35 | mulgneg 19110 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑀 · 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) |
| 37 | 33, 34, 27, 36 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-(𝑀 · 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) |
| 38 | 37 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋)))) |
| 39 | 14, 15 | mulgcl 19109 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵) |
| 40 | 33, 34, 27, 39 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵) |
| 41 | 14, 35 | grpinvinv 19023 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) = ((𝑀 · 𝑁) · 𝑋)) |
| 42 | 40, 41 | syldan 591 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) = ((𝑀 · 𝑁) · 𝑋)) |
| 43 | 38, 42 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((𝑀 · 𝑁) · 𝑋)) |
| 44 | 14, 15 | mulgcl 19109 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 45 | 33, 5, 27, 44 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) ∈ 𝐵) |
| 46 | 14, 15, 35 | mulgneg 19110 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (𝑁 · 𝑋)) = ((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) |
| 47 | 33, 1, 45, 46 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · (𝑁 · 𝑋)) = ((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) |
| 48 | 47 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) = ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋))))) |
| 49 | 14, 15 | mulgcl 19109 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵) |
| 50 | 33, 1, 45, 49 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵) |
| 51 | 14, 35 | grpinvinv 19023 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) = (𝑀 · (𝑁 · 𝑋))) |
| 52 | 50, 51 | syldan 591 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) = (𝑀 · (𝑁 · 𝑋))) |
| 53 | 48, 52 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) = (𝑀 · (𝑁 · 𝑋))) |
| 54 | 43, 53 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) ↔ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 55 | 32, 54 | imbitrid 244 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 56 | 55 | imp 406 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 57 | 31, 56 | syldan 591 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 58 | 57 | ex 412 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 59 | 9 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝐺 ∈
Mnd) |
| 60 | | simprl 771 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝑀 ∈
ℕ0) |
| 61 | | simprr 773 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ -𝑁 ∈
ℕ0) |
| 62 | 27 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝑋 ∈ 𝐵) |
| 63 | 14, 15 | mulgnn0ass 19128 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((𝑀 · -𝑁) · 𝑋) = (𝑀 · (-𝑁 · 𝑋))) |
| 64 | 59, 60, 61, 62, 63 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((𝑀 · -𝑁) · 𝑋) = (𝑀 · (-𝑁 · 𝑋))) |
| 65 | 19, 20 | mulneg2d 11717 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
| 66 | 65 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (𝑀 · -𝑁) = -(𝑀 · 𝑁)) |
| 67 | 66 | oveq1d 7446 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((𝑀 · -𝑁) · 𝑋) = (-(𝑀 · 𝑁) · 𝑋)) |
| 68 | 14, 15, 35 | mulgneg 19110 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
| 69 | 33, 5, 27, 68 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋))) |
| 70 | 69 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (-𝑁 · 𝑋)) = (𝑀 ·
((invg‘𝐺)‘(𝑁 · 𝑋)))) |
| 71 | 14, 15, 35 | mulgneg2 19126 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (𝑁 · 𝑋)) = (𝑀 ·
((invg‘𝐺)‘(𝑁 · 𝑋)))) |
| 72 | 33, 1, 45, 71 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · (𝑁 · 𝑋)) = (𝑀 ·
((invg‘𝐺)‘(𝑁 · 𝑋)))) |
| 73 | 70, 72 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (-𝑁 · 𝑋)) = (-𝑀 · (𝑁 · 𝑋))) |
| 74 | 73 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (𝑀 ·
(-𝑁 · 𝑋)) = (-𝑀 · (𝑁 · 𝑋))) |
| 75 | 64, 67, 74 | 3eqtr3d 2785 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) |
| 76 | 75, 56 | syldan 591 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 77 | 76 | ex 412 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 78 | 9 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝐺 ∈
Mnd) |
| 79 | | simprl 771 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ -𝑀 ∈
ℕ0) |
| 80 | | simprr 773 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ -𝑁 ∈
ℕ0) |
| 81 | 27 | adantr 480 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝑋 ∈ 𝐵) |
| 82 | 14, 15 | mulgnn0ass 19128 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0
∧ -𝑁 ∈
ℕ0 ∧ 𝑋
∈ 𝐵)) → ((-𝑀 · -𝑁) · 𝑋) = (-𝑀 · (-𝑁 · 𝑋))) |
| 83 | 78, 79, 80, 81, 82 | syl13anc 1374 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((-𝑀 · -𝑁) · 𝑋) = (-𝑀 · (-𝑁 · 𝑋))) |
| 84 | 19, 20 | mul2negd 11718 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · -𝑁) = (𝑀 · 𝑁)) |
| 85 | 84 | oveq1d 7446 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 · -𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋)) |
| 86 | 85 | adantr 480 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((-𝑀 · -𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋)) |
| 87 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝐺 ∈
Grp) |
| 88 | 1 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ 𝑀 ∈
ℤ) |
| 89 | | nn0z 12638 |
. . . . . . . . 9
⊢ (-𝑁 ∈ ℕ0
→ -𝑁 ∈
ℤ) |
| 90 | 89 | ad2antll 729 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ -𝑁 ∈
ℤ) |
| 91 | 14, 15 | mulgcl 19109 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) ∈ 𝐵) |
| 92 | 87, 90, 81, 91 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (-𝑁 · 𝑋) ∈ 𝐵) |
| 93 | 14, 15, 35 | mulgneg2 19126 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (-𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (-𝑁 · 𝑋)) = (𝑀 ·
((invg‘𝐺)‘(-𝑁 · 𝑋)))) |
| 94 | 87, 88, 92, 93 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (-𝑀 ·
(-𝑁 · 𝑋)) = (𝑀 ·
((invg‘𝐺)‘(-𝑁 · 𝑋)))) |
| 95 | 14, 15, 35 | mulgneg 19110 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (--𝑁 · 𝑋) = ((invg‘𝐺)‘(-𝑁 · 𝑋))) |
| 96 | 87, 90, 81, 95 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (--𝑁 · 𝑋) =
((invg‘𝐺)‘(-𝑁 · 𝑋))) |
| 97 | 20 | negnegd 11611 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → --𝑁 = 𝑁) |
| 98 | 97 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ --𝑁 = 𝑁) |
| 99 | 98 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (--𝑁 · 𝑋) = (𝑁 · 𝑋)) |
| 100 | 96, 99 | eqtr3d 2779 |
. . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((invg‘𝐺)‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋)) |
| 101 | 100 | oveq2d 7447 |
. . . . . 6
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (𝑀 ·
((invg‘𝐺)‘(-𝑁 · 𝑋))) = (𝑀 · (𝑁 · 𝑋))) |
| 102 | 94, 101 | eqtrd 2777 |
. . . . 5
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ (-𝑀 ·
(-𝑁 · 𝑋)) = (𝑀 · (𝑁 · 𝑋))) |
| 103 | 83, 86, 102 | 3eqtr3d 2785 |
. . . 4
⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0))
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |
| 104 | 103 | ex 412 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)
→ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 105 | 18, 58, 77, 104 | ccased 1039 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (((𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0)
∧ (𝑁 ∈
ℕ0 ∨ -𝑁
∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))) |
| 106 | 4, 8, 105 | mp2and 699 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))) |