| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negeq 11501 | . . . . . . 7
⊢ (𝑥 = 0 → -𝑥 = -0) | 
| 2 |  | neg0 11556 | . . . . . . 7
⊢ -0 =
0 | 
| 3 | 1, 2 | eqtrdi 2792 | . . . . . 6
⊢ (𝑥 = 0 → -𝑥 = 0) | 
| 4 | 3 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = 0 → (-𝑥 · 𝑋) = (0 · 𝑋)) | 
| 5 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = 0 → (𝑥 · (𝐼‘𝑋)) = (0 · (𝐼‘𝑋))) | 
| 6 | 4, 5 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 0 → ((-𝑥 · 𝑋) = (𝑥 · (𝐼‘𝑋)) ↔ (0 · 𝑋) = (0 · (𝐼‘𝑋)))) | 
| 7 |  | negeq 11501 | . . . . . 6
⊢ (𝑥 = 𝑛 → -𝑥 = -𝑛) | 
| 8 | 7 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = 𝑛 → (-𝑥 · 𝑋) = (-𝑛 · 𝑋)) | 
| 9 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = 𝑛 → (𝑥 · (𝐼‘𝑋)) = (𝑛 · (𝐼‘𝑋))) | 
| 10 | 8, 9 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑛 → ((-𝑥 · 𝑋) = (𝑥 · (𝐼‘𝑋)) ↔ (-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)))) | 
| 11 |  | negeq 11501 | . . . . . 6
⊢ (𝑥 = (𝑛 + 1) → -𝑥 = -(𝑛 + 1)) | 
| 12 | 11 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → (-𝑥 · 𝑋) = (-(𝑛 + 1) · 𝑋)) | 
| 13 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = (𝑛 + 1) → (𝑥 · (𝐼‘𝑋)) = ((𝑛 + 1) · (𝐼‘𝑋))) | 
| 14 | 12, 13 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = (𝑛 + 1) → ((-𝑥 · 𝑋) = (𝑥 · (𝐼‘𝑋)) ↔ (-(𝑛 + 1) · 𝑋) = ((𝑛 + 1) · (𝐼‘𝑋)))) | 
| 15 |  | negeq 11501 | . . . . . 6
⊢ (𝑥 = -𝑛 → -𝑥 = --𝑛) | 
| 16 | 15 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = -𝑛 → (-𝑥 · 𝑋) = (--𝑛 · 𝑋)) | 
| 17 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = -𝑛 → (𝑥 · (𝐼‘𝑋)) = (-𝑛 · (𝐼‘𝑋))) | 
| 18 | 16, 17 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = -𝑛 → ((-𝑥 · 𝑋) = (𝑥 · (𝐼‘𝑋)) ↔ (--𝑛 · 𝑋) = (-𝑛 · (𝐼‘𝑋)))) | 
| 19 |  | negeq 11501 | . . . . . 6
⊢ (𝑥 = 𝑁 → -𝑥 = -𝑁) | 
| 20 | 19 | oveq1d 7447 | . . . . 5
⊢ (𝑥 = 𝑁 → (-𝑥 · 𝑋) = (-𝑁 · 𝑋)) | 
| 21 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = 𝑁 → (𝑥 · (𝐼‘𝑋)) = (𝑁 · (𝐼‘𝑋))) | 
| 22 | 20, 21 | eqeq12d 2752 | . . . 4
⊢ (𝑥 = 𝑁 → ((-𝑥 · 𝑋) = (𝑥 · (𝐼‘𝑋)) ↔ (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋)))) | 
| 23 |  | mulgneg2.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐺) | 
| 24 |  | eqid 2736 | . . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 25 |  | mulgneg2.m | . . . . . . 7
⊢  · =
(.g‘𝐺) | 
| 26 | 23, 24, 25 | mulg0 19093 | . . . . . 6
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) | 
| 27 | 26 | adantl 481 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝐺)) | 
| 28 |  | mulgneg2.i | . . . . . . 7
⊢ 𝐼 = (invg‘𝐺) | 
| 29 | 23, 28 | grpinvcl 19006 | . . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) | 
| 30 | 23, 24, 25 | mulg0 19093 | . . . . . 6
⊢ ((𝐼‘𝑋) ∈ 𝐵 → (0 · (𝐼‘𝑋)) = (0g‘𝐺)) | 
| 31 | 29, 30 | syl 17 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · (𝐼‘𝑋)) = (0g‘𝐺)) | 
| 32 | 27, 31 | eqtr4d 2779 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0 · (𝐼‘𝑋))) | 
| 33 |  | oveq1 7439 | . . . . . 6
⊢ ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → ((-𝑛 · 𝑋)(+g‘𝐺)(𝐼‘𝑋)) = ((𝑛 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋))) | 
| 34 |  | nn0cn 12538 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℂ) | 
| 35 | 34 | adantl 481 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℂ) | 
| 36 |  | ax-1cn 11214 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 37 |  | negdi 11567 | . . . . . . . . . 10
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → -(𝑛 + 1) =
(-𝑛 + -1)) | 
| 38 | 35, 36, 37 | sylancl 586 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → -(𝑛 + 1) = (-𝑛 + -1)) | 
| 39 | 38 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (-(𝑛 + 1) · 𝑋) = ((-𝑛 + -1) · 𝑋)) | 
| 40 |  | simpll 766 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝐺 ∈ Grp) | 
| 41 |  | nn0negz 12657 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ -𝑛 ∈
ℤ) | 
| 42 | 41 | adantl 481 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → -𝑛 ∈
ℤ) | 
| 43 |  | 1z 12649 | . . . . . . . . . 10
⊢ 1 ∈
ℤ | 
| 44 |  | znegcl 12654 | . . . . . . . . . 10
⊢ (1 ∈
ℤ → -1 ∈ ℤ) | 
| 45 | 43, 44 | mp1i 13 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → -1 ∈
ℤ) | 
| 46 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑋 ∈ 𝐵) | 
| 47 |  | eqid 2736 | . . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 48 | 23, 25, 47 | mulgdir 19125 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ (-𝑛 ∈ ℤ ∧ -1 ∈
ℤ ∧ 𝑋 ∈
𝐵)) → ((-𝑛 + -1) · 𝑋) = ((-𝑛 · 𝑋)(+g‘𝐺)(-1 · 𝑋))) | 
| 49 | 40, 42, 45, 46, 48 | syl13anc 1373 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((-𝑛 + -1) · 𝑋) = ((-𝑛 · 𝑋)(+g‘𝐺)(-1 · 𝑋))) | 
| 50 | 23, 25, 28 | mulgm1 19113 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (-1 · 𝑋) = (𝐼‘𝑋)) | 
| 51 | 50 | adantr 480 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (-1 · 𝑋) = (𝐼‘𝑋)) | 
| 52 | 51 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((-𝑛 · 𝑋)(+g‘𝐺)(-1 · 𝑋)) = ((-𝑛 · 𝑋)(+g‘𝐺)(𝐼‘𝑋))) | 
| 53 | 39, 49, 52 | 3eqtrd 2780 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (-(𝑛 + 1) · 𝑋) = ((-𝑛 · 𝑋)(+g‘𝐺)(𝐼‘𝑋))) | 
| 54 |  | grpmnd 18959 | . . . . . . . . 9
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) | 
| 55 | 54 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝐺 ∈ Mnd) | 
| 56 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) | 
| 57 | 29 | adantr 480 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → (𝐼‘𝑋) ∈ 𝐵) | 
| 58 | 23, 25, 47 | mulgnn0p1 19104 | . . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑛 ∈ ℕ0
∧ (𝐼‘𝑋) ∈ 𝐵) → ((𝑛 + 1) · (𝐼‘𝑋)) = ((𝑛 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋))) | 
| 59 | 55, 56, 57, 58 | syl3anc 1372 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((𝑛 + 1) · (𝐼‘𝑋)) = ((𝑛 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋))) | 
| 60 | 53, 59 | eqeq12d 2752 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((-(𝑛 + 1) · 𝑋) = ((𝑛 + 1) · (𝐼‘𝑋)) ↔ ((-𝑛 · 𝑋)(+g‘𝐺)(𝐼‘𝑋)) = ((𝑛 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋)))) | 
| 61 | 33, 60 | imbitrrid 246 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) → ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → (-(𝑛 + 1) · 𝑋) = ((𝑛 + 1) · (𝐼‘𝑋)))) | 
| 62 | 61 | ex 412 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑛 ∈ ℕ0 → ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → (-(𝑛 + 1) · 𝑋) = ((𝑛 + 1) · (𝐼‘𝑋))))) | 
| 63 |  | fveq2 6905 | . . . . . 6
⊢ ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → (𝐼‘(-𝑛 · 𝑋)) = (𝐼‘(𝑛 · (𝐼‘𝑋)))) | 
| 64 |  | simpll 766 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝐺 ∈ Grp) | 
| 65 |  | nnnegz 12618 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ → -𝑛 ∈
ℤ) | 
| 66 | 65 | adantl 481 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → -𝑛 ∈ ℤ) | 
| 67 |  | simplr 768 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ 𝐵) | 
| 68 | 23, 25, 28 | mulgneg 19111 | . . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ -𝑛 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (--𝑛 · 𝑋) = (𝐼‘(-𝑛 · 𝑋))) | 
| 69 | 64, 66, 67, 68 | syl3anc 1372 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → (--𝑛 · 𝑋) = (𝐼‘(-𝑛 · 𝑋))) | 
| 70 |  | id 22 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ) | 
| 71 | 23, 25, 28 | mulgnegnn 19103 | . . . . . . . 8
⊢ ((𝑛 ∈ ℕ ∧ (𝐼‘𝑋) ∈ 𝐵) → (-𝑛 · (𝐼‘𝑋)) = (𝐼‘(𝑛 · (𝐼‘𝑋)))) | 
| 72 | 70, 29, 71 | syl2anr 597 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → (-𝑛 · (𝐼‘𝑋)) = (𝐼‘(𝑛 · (𝐼‘𝑋)))) | 
| 73 | 69, 72 | eqeq12d 2752 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → ((--𝑛 · 𝑋) = (-𝑛 · (𝐼‘𝑋)) ↔ (𝐼‘(-𝑛 · 𝑋)) = (𝐼‘(𝑛 · (𝐼‘𝑋))))) | 
| 74 | 63, 73 | imbitrrid 246 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) ∧ 𝑛 ∈ ℕ) → ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → (--𝑛 · 𝑋) = (-𝑛 · (𝐼‘𝑋)))) | 
| 75 | 74 | ex 412 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑛 ∈ ℕ → ((-𝑛 · 𝑋) = (𝑛 · (𝐼‘𝑋)) → (--𝑛 · 𝑋) = (-𝑛 · (𝐼‘𝑋))))) | 
| 76 | 6, 10, 14, 18, 22, 32, 62, 75 | zindd 12721 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ ℤ → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋)))) | 
| 77 | 76 | 3impia 1117 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℤ) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋))) | 
| 78 | 77 | 3com23 1126 | 1
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋))) |