| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 0 → (𝑥 ∙ 𝐵) = (0 ∙ 𝐵)) |
| 2 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 0 → (𝑥 · 𝐵) = (0 · 𝐵)) |
| 3 | 1, 2 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 0 → ((𝑥 ∙ 𝐵) = (𝑥 · 𝐵) ↔ (0 ∙ 𝐵) = (0 · 𝐵))) |
| 4 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ∙ 𝐵) = (𝑦 ∙ 𝐵)) |
| 5 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 · 𝐵) = (𝑦 · 𝐵)) |
| 6 | 4, 5 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 ∙ 𝐵) = (𝑥 · 𝐵) ↔ (𝑦 ∙ 𝐵) = (𝑦 · 𝐵))) |
| 7 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ∙ 𝐵) = ((𝑦 + 1) ∙ 𝐵)) |
| 8 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝐵) = ((𝑦 + 1) · 𝐵)) |
| 9 | 7, 8 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 ∙ 𝐵) = (𝑥 · 𝐵) ↔ ((𝑦 + 1) ∙ 𝐵) = ((𝑦 + 1) · 𝐵))) |
| 10 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = -𝑦 → (𝑥 ∙ 𝐵) = (-𝑦 ∙ 𝐵)) |
| 11 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = -𝑦 → (𝑥 · 𝐵) = (-𝑦 · 𝐵)) |
| 12 | 10, 11 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = -𝑦 → ((𝑥 ∙ 𝐵) = (𝑥 · 𝐵) ↔ (-𝑦 ∙ 𝐵) = (-𝑦 · 𝐵))) |
| 13 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ∙ 𝐵) = (𝐴 ∙ 𝐵)) |
| 14 | | oveq1 7438 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 · 𝐵) = (𝐴 · 𝐵)) |
| 15 | 13, 14 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 ∙ 𝐵) = (𝑥 · 𝐵) ↔ (𝐴 ∙ 𝐵) = (𝐴 · 𝐵))) |
| 16 | | clmmulg.1 |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 18 | | clmmulg.2 |
. . . . . . 7
⊢ ∙ =
(.g‘𝑊) |
| 19 | 16, 17, 18 | mulg0 19092 |
. . . . . 6
⊢ (𝐵 ∈ 𝑉 → (0 ∙ 𝐵) = (0g‘𝑊)) |
| 20 | 19 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (0 ∙ 𝐵) = (0g‘𝑊)) |
| 21 | | eqid 2737 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 22 | | clmmulg.3 |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑊) |
| 23 | 16, 21, 22, 17 | clm0vs 25128 |
. . . . 5
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (0 · 𝐵) = (0g‘𝑊)) |
| 24 | 20, 23 | eqtr4d 2780 |
. . . 4
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (0 ∙ 𝐵) = (0 · 𝐵)) |
| 25 | | oveq1 7438 |
. . . . . 6
⊢ ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → ((𝑦 ∙ 𝐵)(+g‘𝑊)𝐵) = ((𝑦 · 𝐵)(+g‘𝑊)𝐵)) |
| 26 | | clmgrp 25101 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Grp) |
| 27 | 26 | grpmndd 18964 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ Mnd) |
| 28 | 27 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝑊 ∈ Mnd) |
| 29 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
ℕ0) |
| 30 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝐵 ∈ 𝑉) |
| 31 | | eqid 2737 |
. . . . . . . . 9
⊢
(+g‘𝑊) = (+g‘𝑊) |
| 32 | 16, 18, 31 | mulgnn0p1 19103 |
. . . . . . . 8
⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝐵 ∈ 𝑉) → ((𝑦 + 1) ∙ 𝐵) = ((𝑦 ∙ 𝐵)(+g‘𝑊)𝐵)) |
| 33 | 28, 29, 30, 32 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) ∙ 𝐵) = ((𝑦 ∙ 𝐵)(+g‘𝑊)𝐵)) |
| 34 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝑊 ∈
ℂMod) |
| 35 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 36 | 21, 35 | clmzss 25111 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ℂMod →
ℤ ⊆ (Base‘(Scalar‘𝑊))) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ℤ
⊆ (Base‘(Scalar‘𝑊))) |
| 38 | | nn0z 12638 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
| 39 | 38 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
ℤ) |
| 40 | 37, 39 | sseldd 3984 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈
(Base‘(Scalar‘𝑊))) |
| 41 | | 1zzd 12648 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 1 ∈
ℤ) |
| 42 | 37, 41 | sseldd 3984 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → 1 ∈
(Base‘(Scalar‘𝑊))) |
| 43 | 16, 21, 22, 35, 31 | clmvsdir 25124 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℂMod ∧ (𝑦 ∈
(Base‘(Scalar‘𝑊)) ∧ 1 ∈
(Base‘(Scalar‘𝑊)) ∧ 𝐵 ∈ 𝑉)) → ((𝑦 + 1) · 𝐵) = ((𝑦 · 𝐵)(+g‘𝑊)(1 · 𝐵))) |
| 44 | 34, 40, 42, 30, 43 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · 𝐵) = ((𝑦 · 𝐵)(+g‘𝑊)(1 · 𝐵))) |
| 45 | 16, 22 | clmvs1 25126 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (1 · 𝐵) = 𝐵) |
| 46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → (1 · 𝐵) = 𝐵) |
| 47 | 46 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ((𝑦 · 𝐵)(+g‘𝑊)(1 · 𝐵)) = ((𝑦 · 𝐵)(+g‘𝑊)𝐵)) |
| 48 | 44, 47 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ((𝑦 + 1) · 𝐵) = ((𝑦 · 𝐵)(+g‘𝑊)𝐵)) |
| 49 | 33, 48 | eqeq12d 2753 |
. . . . . 6
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → (((𝑦 + 1) ∙ 𝐵) = ((𝑦 + 1) · 𝐵) ↔ ((𝑦 ∙ 𝐵)(+g‘𝑊)𝐵) = ((𝑦 · 𝐵)(+g‘𝑊)𝐵))) |
| 50 | 25, 49 | imbitrrid 246 |
. . . . 5
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ0) → ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → ((𝑦 + 1) ∙ 𝐵) = ((𝑦 + 1) · 𝐵))) |
| 51 | 50 | ex 412 |
. . . 4
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (𝑦 ∈ ℕ0 → ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → ((𝑦 + 1) ∙ 𝐵) = ((𝑦 + 1) · 𝐵)))) |
| 52 | | fveq2 6906 |
. . . . . 6
⊢ ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → ((invg‘𝑊)‘(𝑦 ∙ 𝐵)) = ((invg‘𝑊)‘(𝑦 · 𝐵))) |
| 53 | 26 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → 𝑊 ∈ Grp) |
| 54 | | nnz 12634 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 55 | 54 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℤ) |
| 56 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → 𝐵 ∈ 𝑉) |
| 57 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘𝑊) = (invg‘𝑊) |
| 58 | 16, 18, 57 | mulgneg 19110 |
. . . . . . . 8
⊢ ((𝑊 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (-𝑦 ∙ 𝐵) = ((invg‘𝑊)‘(𝑦 ∙ 𝐵))) |
| 59 | 53, 55, 56, 58 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → (-𝑦 ∙ 𝐵) = ((invg‘𝑊)‘(𝑦 ∙ 𝐵))) |
| 60 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → 𝑊 ∈ ℂMod) |
| 61 | 36 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → ℤ ⊆
(Base‘(Scalar‘𝑊))) |
| 62 | 61, 55 | sseldd 3984 |
. . . . . . . . 9
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ (Base‘(Scalar‘𝑊))) |
| 63 | 16, 21, 22, 57, 35, 60, 56, 62 | clmvsneg 25133 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) →
((invg‘𝑊)‘(𝑦 · 𝐵)) = (-𝑦 · 𝐵)) |
| 64 | 63 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → (-𝑦 · 𝐵) = ((invg‘𝑊)‘(𝑦 · 𝐵))) |
| 65 | 59, 64 | eqeq12d 2753 |
. . . . . 6
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → ((-𝑦 ∙ 𝐵) = (-𝑦 · 𝐵) ↔ ((invg‘𝑊)‘(𝑦 ∙ 𝐵)) = ((invg‘𝑊)‘(𝑦 · 𝐵)))) |
| 66 | 52, 65 | imbitrrid 246 |
. . . . 5
⊢ (((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) ∧ 𝑦 ∈ ℕ) → ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → (-𝑦 ∙ 𝐵) = (-𝑦 · 𝐵))) |
| 67 | 66 | ex 412 |
. . . 4
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (𝑦 ∈ ℕ → ((𝑦 ∙ 𝐵) = (𝑦 · 𝐵) → (-𝑦 ∙ 𝐵) = (-𝑦 · 𝐵)))) |
| 68 | 3, 6, 9, 12, 15, 24, 51, 67 | zindd 12719 |
. . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉) → (𝐴 ∈ ℤ → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵))) |
| 69 | 68 | 3impia 1118 |
. 2
⊢ ((𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ ℤ) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵)) |
| 70 | 69 | 3com23 1127 |
1
⊢ ((𝑊 ∈ ℂMod ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ 𝑉) → (𝐴 ∙ 𝐵) = (𝐴 · 𝐵)) |