Step | Hyp | Ref
| Expression |
1 | | cpmidpmat.g |
. 2
⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐾)‘𝑘) ∗ 𝑂)) |
2 | | fvex 6113 |
. . . 4
⊢
(0g‘𝐴) ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0g‘𝐴) ∈ V) |
4 | | ovex 6577 |
. . . 4
⊢
(((coe1‘𝐾)‘𝑘) ∗ 𝑂) ∈ V |
5 | 4 | a1i 11 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) →
(((coe1‘𝐾)‘𝑘) ∗ 𝑂) ∈ V) |
6 | | fveq2 6103 |
. . . 4
⊢ (𝑘 = 𝑙 → ((coe1‘𝐾)‘𝑘) = ((coe1‘𝐾)‘𝑙)) |
7 | 6 | oveq1d 6564 |
. . 3
⊢ (𝑘 = 𝑙 → (((coe1‘𝐾)‘𝑘) ∗ 𝑂) = (((coe1‘𝐾)‘𝑙) ∗ 𝑂)) |
8 | | fvex 6113 |
. . . . . 6
⊢
(0g‘𝑅) ∈ V |
9 | 8 | a1i 11 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (0g‘𝑅) ∈ V) |
10 | | cpmidgsum.k |
. . . . . . 7
⊢ 𝐾 = (𝐶‘𝑀) |
11 | | cpmidgsum.c |
. . . . . . . 8
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
12 | | cpmidgsum.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
13 | | cpmidgsum.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
14 | | cpmidgsum.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝑃) =
(Base‘𝑃) |
16 | 11, 12, 13, 14, 15 | chpmatply1 20456 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ (Base‘𝑃)) |
17 | 10, 16 | syl5eqel 2692 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐾 ∈ (Base‘𝑃)) |
18 | | eqid 2610 |
. . . . . . 7
⊢
(coe1‘𝐾) = (coe1‘𝐾) |
19 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
20 | 18, 15, 14, 19 | coe1fvalcl 19403 |
. . . . . 6
⊢ ((𝐾 ∈ (Base‘𝑃) ∧ 𝑛 ∈ ℕ0) →
((coe1‘𝐾)‘𝑛) ∈ (Base‘𝑅)) |
21 | 17, 20 | sylan 487 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) →
((coe1‘𝐾)‘𝑛) ∈ (Base‘𝑅)) |
22 | | crngring 18381 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
23 | 22 | 3ad2ant2 1076 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
24 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
25 | 14, 15, 24 | mptcoe1fsupp 19406 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐾 ∈ (Base‘𝑃)) → (𝑛 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑛)) finSupp (0g‘𝑅)) |
26 | 23, 17, 25 | syl2anc 691 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑛 ∈ ℕ0 ↦
((coe1‘𝐾)‘𝑛)) finSupp (0g‘𝑅)) |
27 | 9, 21, 26 | mptnn0fsuppr 12661 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑙 ∈ ℕ0
(𝑠 < 𝑙 → ⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅))) |
28 | | csbfv 6143 |
. . . . . . . . . . . . . 14
⊢
⦋𝑙 /
𝑛⦌((coe1‘𝐾)‘𝑛) = ((coe1‘𝐾)‘𝑙) |
29 | 28 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) →
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = ((coe1‘𝐾)‘𝑙)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) →
(⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅) ↔ ((coe1‘𝐾)‘𝑙) = (0g‘𝑅))) |
31 | 30 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → ((coe1‘𝐾)‘𝑙) = (0g‘𝑅)) |
32 | 12 | matsca2 20045 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝐴)) |
33 | 32 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 = (Scalar‘𝐴)) |
34 | 33 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → 𝑅 = (Scalar‘𝐴)) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → (0g‘𝑅) =
(0g‘(Scalar‘𝐴))) |
36 | 31, 35 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → ((coe1‘𝐾)‘𝑙) = (0g‘(Scalar‘𝐴))) |
37 | 36 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) =
((0g‘(Scalar‘𝐴)) ∗ 𝑂)) |
38 | 12 | matlmod 20054 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ LMod) |
39 | 22, 38 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ LMod) |
40 | 39 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ LMod) |
41 | 12 | matring 20068 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
42 | 22, 41 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
43 | | cpmidgsumm2pm.o |
. . . . . . . . . . . . . 14
⊢ 𝑂 = (1r‘𝐴) |
44 | 13, 43 | ringidcl 18391 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Ring → 𝑂 ∈ 𝐵) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑂 ∈ 𝐵) |
46 | 45 | 3adant3 1074 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑂 ∈ 𝐵) |
47 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Scalar‘𝐴) =
(Scalar‘𝐴) |
48 | | cpmidgsumm2pm.m |
. . . . . . . . . . . 12
⊢ ∗ = (
·𝑠 ‘𝐴) |
49 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(Scalar‘𝐴)) =
(0g‘(Scalar‘𝐴)) |
50 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘𝐴) = (0g‘𝐴) |
51 | 13, 47, 48, 49, 50 | lmod0vs 18719 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ LMod ∧ 𝑂 ∈ 𝐵) →
((0g‘(Scalar‘𝐴)) ∗ 𝑂) = (0g‘𝐴)) |
52 | 40, 46, 51 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) →
((0g‘(Scalar‘𝐴)) ∗ 𝑂) = (0g‘𝐴)) |
53 | 52 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) →
((0g‘(Scalar‘𝐴)) ∗ 𝑂) = (0g‘𝐴)) |
54 | 37, 53 | eqtrd 2644 |
. . . . . . . 8
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) ∧
⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴)) |
55 | 54 | ex 449 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) →
(⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅) → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴))) |
56 | 55 | imim2d 55 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑙 ∈ ℕ0) → ((𝑠 < 𝑙 → ⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → (𝑠 < 𝑙 → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴)))) |
57 | 56 | ralimdva 2945 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∀𝑙 ∈ ℕ0 (𝑠 < 𝑙 → ⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → ∀𝑙 ∈ ℕ0 (𝑠 < 𝑙 → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴)))) |
58 | 57 | reximdv 2999 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑠 ∈ ℕ0 ∀𝑙 ∈ ℕ0
(𝑠 < 𝑙 → ⦋𝑙 / 𝑛⦌((coe1‘𝐾)‘𝑛) = (0g‘𝑅)) → ∃𝑠 ∈ ℕ0 ∀𝑙 ∈ ℕ0
(𝑠 < 𝑙 → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴)))) |
59 | 27, 58 | mpd 15 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∀𝑙 ∈ ℕ0
(𝑠 < 𝑙 → (((coe1‘𝐾)‘𝑙) ∗ 𝑂) = (0g‘𝐴))) |
60 | 3, 5, 7, 59 | mptnn0fsuppd 12660 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦
(((coe1‘𝐾)‘𝑘) ∗ 𝑂)) finSupp (0g‘𝐴)) |
61 | 1, 60 | syl5eqbr 4618 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺 finSupp (0g‘𝐴)) |