Proof of Theorem chpdmatlem3
| Step | Hyp | Ref
| Expression |
| 1 | | chpdmat.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
| 2 | 1 | ply1ring 22249 |
. . . . 5
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 3 | 2 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring) |
| 4 | 3 | adantr 480 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → 𝑃 ∈ Ring) |
| 5 | | chpdmat.c |
. . . . . . 7
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
| 6 | | chpdmat.a |
. . . . . . 7
⊢ 𝐴 = (𝑁 Mat 𝑅) |
| 7 | | chpdmat.s |
. . . . . . 7
⊢ 𝑆 = (algSc‘𝑃) |
| 8 | | chpdmat.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
| 9 | | chpdmat.x |
. . . . . . 7
⊢ 𝑋 = (var1‘𝑅) |
| 10 | | chpdmat.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
| 11 | | chpdmat.g |
. . . . . . 7
⊢ 𝐺 = (mulGrp‘𝑃) |
| 12 | | chpdmat.m |
. . . . . . 7
⊢ − =
(-g‘𝑃) |
| 13 | | chpdmatlem.q |
. . . . . . 7
⊢ 𝑄 = (𝑁 Mat 𝑃) |
| 14 | | chpdmatlem.1 |
. . . . . . 7
⊢ 1 =
(1r‘𝑄) |
| 15 | | chpdmatlem.m |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑄) |
| 16 | 5, 1, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15 | chpdmatlem0 22843 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 · 1 ) ∈ (Base‘𝑄)) |
| 17 | 16 | 3adant3 1133 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑋 · 1 ) ∈ (Base‘𝑄)) |
| 18 | | chpdmatlem.t |
. . . . . 6
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
| 19 | 18, 6, 8, 1, 13 | mat2pmatbas 22732 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑄)) |
| 20 | 17, 19 | jca 511 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑋 · 1 ) ∈ (Base‘𝑄) ∧ (𝑇‘𝑀) ∈ (Base‘𝑄))) |
| 21 | 20 | adantr 480 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → ((𝑋 · 1 ) ∈ (Base‘𝑄) ∧ (𝑇‘𝑀) ∈ (Base‘𝑄))) |
| 22 | | simpr 484 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → 𝐾 ∈ 𝑁) |
| 23 | | eqid 2737 |
. . . 4
⊢
(Base‘𝑄) =
(Base‘𝑄) |
| 24 | | chpdmatlem.z |
. . . 4
⊢ 𝑍 = (-g‘𝑄) |
| 25 | 13, 23, 24, 12 | matsubgcell 22440 |
. . 3
⊢ ((𝑃 ∈ Ring ∧ ((𝑋 · 1 ) ∈ (Base‘𝑄) ∧ (𝑇‘𝑀) ∈ (Base‘𝑄)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → (𝐾((𝑋 · 1 )𝑍(𝑇‘𝑀))𝐾) = ((𝐾(𝑋 · 1 )𝐾) − (𝐾(𝑇‘𝑀)𝐾))) |
| 26 | 4, 21, 22, 22, 25 | syl112anc 1376 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾((𝑋 · 1 )𝑍(𝑇‘𝑀))𝐾) = ((𝐾(𝑋 · 1 )𝐾) − (𝐾(𝑇‘𝑀)𝐾))) |
| 27 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑃) =
(Base‘𝑃) |
| 28 | 9, 1, 27 | vr1cl 22219 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
| 29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑋 ∈ (Base‘𝑃)) |
| 30 | 1, 13 | pmatring 22698 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ Ring) |
| 31 | 23, 14 | ringidcl 20262 |
. . . . . . . . 9
⊢ (𝑄 ∈ Ring → 1 ∈
(Base‘𝑄)) |
| 32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 1 ∈
(Base‘𝑄)) |
| 33 | 29, 32 | jca 511 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 ∈ (Base‘𝑃) ∧ 1 ∈ (Base‘𝑄))) |
| 34 | 33 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑋 ∈ (Base‘𝑃) ∧ 1 ∈ (Base‘𝑄))) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝑋 ∈ (Base‘𝑃) ∧ 1 ∈ (Base‘𝑄))) |
| 36 | | eqid 2737 |
. . . . . 6
⊢
(.r‘𝑃) = (.r‘𝑃) |
| 37 | 13, 23, 27, 15, 36 | matvscacell 22442 |
. . . . 5
⊢ ((𝑃 ∈ Ring ∧ (𝑋 ∈ (Base‘𝑃) ∧ 1 ∈ (Base‘𝑄)) ∧ (𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → (𝐾(𝑋 · 1 )𝐾) = (𝑋(.r‘𝑃)(𝐾 1 𝐾))) |
| 38 | 4, 35, 22, 22, 37 | syl112anc 1376 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾(𝑋 · 1 )𝐾) = (𝑋(.r‘𝑃)(𝐾 1 𝐾))) |
| 39 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘𝑃) = (1r‘𝑃) |
| 40 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑃) = (0g‘𝑃) |
| 41 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → 𝑁 ∈ Fin) |
| 42 | 13, 39, 40, 41, 4, 22, 22, 14 | mat1ov 22454 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾 1 𝐾) = if(𝐾 = 𝐾, (1r‘𝑃), (0g‘𝑃))) |
| 43 | | eqid 2737 |
. . . . . . 7
⊢ 𝐾 = 𝐾 |
| 44 | 43 | iftruei 4532 |
. . . . . 6
⊢ if(𝐾 = 𝐾, (1r‘𝑃), (0g‘𝑃)) = (1r‘𝑃) |
| 45 | 42, 44 | eqtrdi 2793 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾 1 𝐾) = (1r‘𝑃)) |
| 46 | 45 | oveq2d 7447 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝑋(.r‘𝑃)(𝐾 1 𝐾)) = (𝑋(.r‘𝑃)(1r‘𝑃))) |
| 47 | 2, 28 | jca 511 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (𝑃 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑃))) |
| 48 | 47 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑃 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑃))) |
| 49 | 27, 36, 39 | ringridm 20267 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ 𝑋 ∈ (Base‘𝑃)) → (𝑋(.r‘𝑃)(1r‘𝑃)) = 𝑋) |
| 50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑋(.r‘𝑃)(1r‘𝑃)) = 𝑋) |
| 51 | 50 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝑋(.r‘𝑃)(1r‘𝑃)) = 𝑋) |
| 52 | 38, 46, 51 | 3eqtrd 2781 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾(𝑋 · 1 )𝐾) = 𝑋) |
| 53 | 18, 6, 8, 1, 7 | mat2pmatvalel 22731 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁)) → (𝐾(𝑇‘𝑀)𝐾) = (𝑆‘(𝐾𝑀𝐾))) |
| 54 | 53 | anabsan2 674 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾(𝑇‘𝑀)𝐾) = (𝑆‘(𝐾𝑀𝐾))) |
| 55 | 52, 54 | oveq12d 7449 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → ((𝐾(𝑋 · 1 )𝐾) − (𝐾(𝑇‘𝑀)𝐾)) = (𝑋 − (𝑆‘(𝐾𝑀𝐾)))) |
| 56 | 26, 55 | eqtrd 2777 |
1
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾((𝑋 · 1 )𝑍(𝑇‘𝑀))𝐾) = (𝑋 − (𝑆‘(𝐾𝑀𝐾)))) |