Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑁 ∈ Fin) |
2 | | simpr 488 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing) |
3 | | crngring 19574 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
4 | | chp0mat.a |
. . . . . 6
⊢ 𝐴 = (𝑁 Mat 𝑅) |
5 | 4 | matring 21340 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
6 | 3, 5 | sylan2 596 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring) |
7 | | ringgrp 19567 |
. . . 4
⊢ (𝐴 ∈ Ring → 𝐴 ∈ Grp) |
8 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐴) =
(Base‘𝐴) |
9 | | chp0mat.0 |
. . . . 5
⊢ 0 =
(0g‘𝐴) |
10 | 8, 9 | grpidcl 18395 |
. . . 4
⊢ (𝐴 ∈ Grp → 0 ∈
(Base‘𝐴)) |
11 | 6, 7, 10 | 3syl 18 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 0 ∈
(Base‘𝐴)) |
12 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
13 | 4, 12 | mat0op 21316 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(0g‘𝐴) =
(𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
14 | 9, 13 | syl5eq 2790 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 0 = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
15 | 3, 14 | sylan2 596 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 0 = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
16 | 15 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 0 = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
17 | | eqidd 2738 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑥 = 𝑖 ∧ 𝑦 = 𝑗)) → (0g‘𝑅) = (0g‘𝑅)) |
18 | | simpl 486 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁) |
19 | 18 | adantl 485 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑖 ∈ 𝑁) |
20 | | simpr 488 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁) |
21 | 20 | adantl 485 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑗 ∈ 𝑁) |
22 | | fvexd 6732 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (0g‘𝑅) ∈ V) |
23 | 16, 17, 19, 21, 22 | ovmpod 7361 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 0 𝑗) = (0g‘𝑅)) |
24 | 23 | a1d 25 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ≠ 𝑗 → (𝑖 0 𝑗) = (0g‘𝑅))) |
25 | 24 | ralrimivva 3112 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖 0 𝑗) = (0g‘𝑅))) |
26 | | chp0mat.c |
. . . 4
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
27 | | chp0mat.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
28 | | eqid 2737 |
. . . 4
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
29 | | chp0mat.x |
. . . 4
⊢ 𝑋 = (var1‘𝑅) |
30 | | chp0mat.g |
. . . 4
⊢ 𝐺 = (mulGrp‘𝑃) |
31 | | eqid 2737 |
. . . 4
⊢
(-g‘𝑃) = (-g‘𝑃) |
32 | 26, 27, 4, 28, 8, 29, 12, 30, 31 | chpdmat 21738 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 0 ∈
(Base‘𝐴)) ∧
∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖 0 𝑗) = (0g‘𝑅))) → (𝐶‘ 0 ) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘)))))) |
33 | 1, 2, 11, 25, 32 | syl31anc 1375 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘ 0 ) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘)))))) |
34 | 15 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → 0 = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (0g‘𝑅))) |
35 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) ∧ (𝑥 = 𝑘 ∧ 𝑦 = 𝑘)) → (0g‘𝑅) = (0g‘𝑅)) |
36 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → 𝑘 ∈ 𝑁) |
37 | | fvexd 6732 |
. . . . . . . . 9
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (0g‘𝑅) ∈ V) |
38 | 34, 35, 36, 36, 37 | ovmpod 7361 |
. . . . . . . 8
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (𝑘 0 𝑘) = (0g‘𝑅)) |
39 | 38 | fveq2d 6721 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘 0 𝑘)) = ((algSc‘𝑃)‘(0g‘𝑅))) |
40 | 3 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring) |
41 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑃) = (0g‘𝑃) |
42 | 27, 28, 12, 41 | ply1scl0 21211 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
((algSc‘𝑃)‘(0g‘𝑅)) = (0g‘𝑃)) |
43 | 40, 42 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) →
((algSc‘𝑃)‘(0g‘𝑅)) = (0g‘𝑃)) |
44 | 43 | adantr 484 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → ((algSc‘𝑃)‘(0g‘𝑅)) = (0g‘𝑃)) |
45 | 39, 44 | eqtrd 2777 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘 0 𝑘)) = (0g‘𝑃)) |
46 | 45 | oveq2d 7229 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘))) = (𝑋(-g‘𝑃)(0g‘𝑃))) |
47 | 27 | ply1ring 21169 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
48 | | ringgrp 19567 |
. . . . . . . . . 10
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
49 | 3, 47, 48 | 3syl 18 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Grp) |
50 | 49 | adantl 485 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Grp) |
51 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘𝑃) |
52 | 29, 27, 51 | vr1cl 21138 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
53 | 40, 52 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝑃)) |
54 | 50, 53 | jca 515 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃))) |
55 | 54 | adantr 484 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃))) |
56 | 51, 41, 31 | grpsubid1 18448 |
. . . . . 6
⊢ ((𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃)) → (𝑋(-g‘𝑃)(0g‘𝑃)) = 𝑋) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (𝑋(-g‘𝑃)(0g‘𝑃)) = 𝑋) |
58 | 46, 57 | eqtrd 2777 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘 ∈ 𝑁) → (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘))) = 𝑋) |
59 | 58 | mpteq2dva 5150 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑘 ∈ 𝑁 ↦ (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘)))) = (𝑘 ∈ 𝑁 ↦ 𝑋)) |
60 | 59 | oveq2d 7229 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐺 Σg
(𝑘 ∈ 𝑁 ↦ (𝑋(-g‘𝑃)((algSc‘𝑃)‘(𝑘 0 𝑘))))) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ 𝑋))) |
61 | 27 | ply1crng 21119 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
62 | 30 | crngmgp 19570 |
. . . . 5
⊢ (𝑃 ∈ CRing → 𝐺 ∈ CMnd) |
63 | | cmnmnd 19186 |
. . . . 5
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
64 | 61, 62, 63 | 3syl 18 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝐺 ∈ Mnd) |
65 | 64 | adantl 485 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐺 ∈ Mnd) |
66 | 3, 52 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑋 ∈ (Base‘𝑃)) |
67 | 66 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝑃)) |
68 | 30, 51 | mgpbas 19510 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝐺) |
69 | 67, 68 | eleqtrdi 2848 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑋 ∈ (Base‘𝐺)) |
70 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
71 | | chp0mat.m |
. . . 4
⊢ ↑ =
(.g‘𝐺) |
72 | 70, 71 | gsumconst 19319 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ 𝑋 ∈ (Base‘𝐺)) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ 𝑋)) = ((♯‘𝑁) ↑ 𝑋)) |
73 | 65, 1, 69, 72 | syl3anc 1373 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐺 Σg
(𝑘 ∈ 𝑁 ↦ 𝑋)) = ((♯‘𝑁) ↑ 𝑋)) |
74 | 33, 60, 73 | 3eqtrd 2781 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘ 0 ) = ((♯‘𝑁) ↑ 𝑋)) |