Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝑁 ∈ Fin) |
2 | | simplr 769 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝑅 ∈ CRing) |
3 | | elrabi 3579 |
. . . . . 6
⊢ (𝑀 ∈ {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} → 𝑀 ∈ (Base‘𝐴)) |
4 | | chpscmat.d |
. . . . . 6
⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} |
5 | 3, 4 | eleq2s 2851 |
. . . . 5
⊢ (𝑀 ∈ 𝐷 → 𝑀 ∈ (Base‘𝐴)) |
6 | 5 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸) → 𝑀 ∈ (Base‘𝐴)) |
7 | 6 | adantl 485 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝑀 ∈ (Base‘𝐴)) |
8 | | oveq 7170 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑀 → (𝑖𝑚𝑗) = (𝑖𝑀𝑗)) |
9 | 8 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑀 → ((𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) ↔ (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)))) |
10 | 9 | 2ralbidv 3111 |
. . . . . . . . 9
⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)))) |
11 | 10 | rexbidv 3206 |
. . . . . . . 8
⊢ (𝑚 = 𝑀 → (∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) ↔ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)))) |
12 | 11 | elrab 3585 |
. . . . . . 7
⊢ (𝑀 ∈ {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} ↔ (𝑀 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)))) |
13 | | ifnefalse 4423 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ≠ 𝑗 → if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) = (0g‘𝑅)) |
14 | 13 | eqeq2d 2749 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ≠ 𝑗 → ((𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) ↔ (𝑖𝑀𝑗) = (0g‘𝑅))) |
15 | 14 | biimpcd 252 |
. . . . . . . . . . . . . 14
⊢ ((𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))) |
16 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((((𝑀 ∈
(Base‘𝐴) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) → ((𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
17 | 16 | ralimdva 3091 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ (Base‘𝐴) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝑖 ∈ 𝑁) → (∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
18 | 17 | ralimdva 3091 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ (Base‘𝐴) ∧ 𝑐 ∈ (Base‘𝑅)) ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
19 | 18 | ex 416 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ (Base‘𝐴) ∧ 𝑐 ∈ (Base‘𝑅)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))))) |
20 | 19 | com23 86 |
. . . . . . . . 9
⊢ ((𝑀 ∈ (Base‘𝐴) ∧ 𝑐 ∈ (Base‘𝑅)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))))) |
21 | 20 | rexlimdva 3193 |
. . . . . . . 8
⊢ (𝑀 ∈ (Base‘𝐴) → (∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))))) |
22 | 21 | imp 410 |
. . . . . . 7
⊢ ((𝑀 ∈ (Base‘𝐴) ∧ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑀𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
23 | 12, 22 | sylbi 220 |
. . . . . 6
⊢ (𝑀 ∈ {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
24 | 23, 4 | eleq2s 2851 |
. . . . 5
⊢ (𝑀 ∈ 𝐷 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
25 | 24 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅)))) |
26 | 25 | impcom 411 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))) |
27 | | chp0mat.c |
. . . 4
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
28 | | chp0mat.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
29 | | chp0mat.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
30 | | chpscmat.s |
. . . 4
⊢ 𝑆 = (algSc‘𝑃) |
31 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐴) =
(Base‘𝐴) |
32 | | chp0mat.x |
. . . 4
⊢ 𝑋 = (var1‘𝑅) |
33 | | eqid 2738 |
. . . 4
⊢
(0g‘𝑅) = (0g‘𝑅) |
34 | | chp0mat.g |
. . . 4
⊢ 𝐺 = (mulGrp‘𝑃) |
35 | | chpscmat.m |
. . . 4
⊢ − =
(-g‘𝑃) |
36 | 27, 28, 29, 30, 31, 32, 33, 34, 35 | chpdmat 21585 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ (Base‘𝐴)) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = (0g‘𝑅))) → (𝐶‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘)))))) |
37 | 1, 2, 7, 26, 36 | syl31anc 1374 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐶‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘)))))) |
38 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → 𝑛 = 𝑘) |
39 | 38, 38 | oveq12d 7182 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (𝑛𝑀𝑛) = (𝑘𝑀𝑘)) |
40 | 39 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → ((𝑛𝑀𝑛) = 𝐸 ↔ (𝑘𝑀𝑘) = 𝐸)) |
41 | 40 | rspccv 3521 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
𝑁 (𝑛𝑀𝑛) = 𝐸 → (𝑘 ∈ 𝑁 → (𝑘𝑀𝑘) = 𝐸)) |
42 | 41 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸) → (𝑘 ∈ 𝑁 → (𝑘𝑀𝑘) = 𝐸)) |
43 | 42 | adantl 485 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝑘 ∈ 𝑁 → (𝑘𝑀𝑘) = 𝐸)) |
44 | 43 | imp 410 |
. . . . . 6
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) ∧ 𝑘 ∈ 𝑁) → (𝑘𝑀𝑘) = 𝐸) |
45 | 44 | fveq2d 6672 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) ∧ 𝑘 ∈ 𝑁) → (𝑆‘(𝑘𝑀𝑘)) = (𝑆‘𝐸)) |
46 | 45 | oveq2d 7180 |
. . . 4
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) ∧ 𝑘 ∈ 𝑁) → (𝑋 − (𝑆‘(𝑘𝑀𝑘))) = (𝑋 − (𝑆‘𝐸))) |
47 | 46 | mpteq2dva 5122 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘)))) = (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘𝐸)))) |
48 | 47 | oveq2d 7180 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘))))) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘𝐸))))) |
49 | 28 | ply1crng 20966 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
50 | 34 | crngmgp 19417 |
. . . . 5
⊢ (𝑃 ∈ CRing → 𝐺 ∈ CMnd) |
51 | | cmnmnd 19033 |
. . . . 5
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
52 | 49, 50, 51 | 3syl 18 |
. . . 4
⊢ (𝑅 ∈ CRing → 𝐺 ∈ Mnd) |
53 | 52 | ad2antlr 727 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝐺 ∈ Mnd) |
54 | | crngring 19421 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
55 | 28 | ply1ring 21016 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
56 | 54, 55 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
57 | | ringgrp 19414 |
. . . . . . 7
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) |
58 | 56, 57 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Grp) |
59 | 58 | ad2antlr 727 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝑃 ∈ Grp) |
60 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘𝑃) =
(Base‘𝑃) |
61 | 32, 28, 60 | vr1cl 20985 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
62 | 54, 61 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑋 ∈ (Base‘𝑃)) |
63 | 62 | ad2antlr 727 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → 𝑋 ∈ (Base‘𝑃)) |
64 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝐼 ∈ 𝑁) |
65 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
66 | 56 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → 𝑃 ∈ Ring) |
67 | 66 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝑃 ∈ Ring) |
68 | 28 | ply1lmod 21020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
69 | 54, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 ∈ CRing → 𝑃 ∈ LMod) |
70 | 69 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → 𝑃 ∈ LMod) |
71 | 70 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝑃 ∈ LMod) |
72 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
73 | 30, 65, 67, 71, 72, 60 | asclf 20688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝑆:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)) |
74 | 5 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → 𝑀 ∈ (Base‘𝐴)) |
75 | 74 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝑀 ∈ (Base‘𝐴)) |
76 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Base‘𝑅) =
(Base‘𝑅) |
77 | 29, 76 | matecl 21169 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑁 ∧ 𝐼 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
78 | 64, 64, 75, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (𝐼𝑀𝐼) ∈ (Base‘𝑅)) |
79 | 28 | ply1sca 21021 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
80 | 79 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → 𝑅 = (Scalar‘𝑃)) |
81 | 80 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → 𝑅 = (Scalar‘𝑃)) |
82 | 81 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (Scalar‘𝑃) = 𝑅) |
83 | 82 | fveq2d 6672 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (Base‘(Scalar‘𝑃)) = (Base‘𝑅)) |
84 | 78, 83 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (𝐼𝑀𝐼) ∈ (Base‘(Scalar‘𝑃))) |
85 | 73, 84 | ffvelrnd 6856 |
. . . . . . . . . . . . . . 15
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (𝑆‘(𝐼𝑀𝐼)) ∈ (Base‘𝑃)) |
86 | | fveq2 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 = (𝐼𝑀𝐼) → (𝑆‘𝐸) = (𝑆‘(𝐼𝑀𝐼))) |
87 | 86 | eqcoms 2746 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼𝑀𝐼) = 𝐸 → (𝑆‘𝐸) = (𝑆‘(𝐼𝑀𝐼))) |
88 | 87 | eleq1d 2817 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼𝑀𝐼) = 𝐸 → ((𝑆‘𝐸) ∈ (Base‘𝑃) ↔ (𝑆‘(𝐼𝑀𝐼)) ∈ (Base‘𝑃))) |
89 | 85, 88 | syl5ibrcom 250 |
. . . . . . . . . . . . . 14
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → ((𝐼𝑀𝐼) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃))) |
90 | 89 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) ∧ 𝑛 = 𝐼) → ((𝐼𝑀𝐼) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃))) |
91 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝐼 → 𝑛 = 𝐼) |
92 | 91, 91 | oveq12d 7182 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝐼 → (𝑛𝑀𝑛) = (𝐼𝑀𝐼)) |
93 | 92 | eqeq1d 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝐼 → ((𝑛𝑀𝑛) = 𝐸 ↔ (𝐼𝑀𝐼) = 𝐸)) |
94 | 93 | imbi1d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝐼 → (((𝑛𝑀𝑛) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃)) ↔ ((𝐼𝑀𝐼) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃)))) |
95 | 94 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) ∧ 𝑛 = 𝐼) → (((𝑛𝑀𝑛) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃)) ↔ ((𝐼𝑀𝐼) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃)))) |
96 | 90, 95 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) ∧ 𝑛 = 𝐼) → ((𝑛𝑀𝑛) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃))) |
97 | 64, 96 | rspcimdv 3514 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) ∧ 𝐼 ∈ 𝑁) → (∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃))) |
98 | 97 | ex 416 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → (𝐼 ∈ 𝑁 → (∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸 → (𝑆‘𝐸) ∈ (Base‘𝑃)))) |
99 | 98 | com23 86 |
. . . . . . . . 9
⊢ ((𝑀 ∈ 𝐷 ∧ (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing)) → (∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸 → (𝐼 ∈ 𝑁 → (𝑆‘𝐸) ∈ (Base‘𝑃)))) |
100 | 99 | ex 416 |
. . . . . . . 8
⊢ (𝑀 ∈ 𝐷 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸 → (𝐼 ∈ 𝑁 → (𝑆‘𝐸) ∈ (Base‘𝑃))))) |
101 | 100 | com24 95 |
. . . . . . 7
⊢ (𝑀 ∈ 𝐷 → (𝐼 ∈ 𝑁 → (∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸 → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑆‘𝐸) ∈ (Base‘𝑃))))) |
102 | 101 | 3imp 1112 |
. . . . . 6
⊢ ((𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑆‘𝐸) ∈ (Base‘𝑃))) |
103 | 102 | impcom 411 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝑆‘𝐸) ∈ (Base‘𝑃)) |
104 | 60, 35 | grpsubcl 18290 |
. . . . 5
⊢ ((𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃) ∧ (𝑆‘𝐸) ∈ (Base‘𝑃)) → (𝑋 − (𝑆‘𝐸)) ∈ (Base‘𝑃)) |
105 | 59, 63, 103, 104 | syl3anc 1372 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝑋 − (𝑆‘𝐸)) ∈ (Base‘𝑃)) |
106 | 34, 60 | mgpbas 19357 |
. . . 4
⊢
(Base‘𝑃) =
(Base‘𝐺) |
107 | 105, 106 | eleqtrdi 2843 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝑋 − (𝑆‘𝐸)) ∈ (Base‘𝐺)) |
108 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
109 | | chp0mat.m |
. . . 4
⊢ ↑ =
(.g‘𝐺) |
110 | 108, 109 | gsumconst 19166 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ (𝑋 − (𝑆‘𝐸)) ∈ (Base‘𝐺)) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘𝐸)))) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘𝐸)))) |
111 | 53, 1, 107, 110 | syl3anc 1372 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘𝐸)))) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘𝐸)))) |
112 | 37, 48, 111 | 3eqtrd 2777 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐶‘𝑀) = ((♯‘𝑁) ↑ (𝑋 − (𝑆‘𝐸)))) |