Proof of Theorem chpmat1d
Step | Hyp | Ref
| Expression |
1 | | snfi 8821 |
. . . . . 6
⊢ {𝐼} ∈ Fin |
2 | | eleq1 2826 |
. . . . . 6
⊢ (𝑁 = {𝐼} → (𝑁 ∈ Fin ↔ {𝐼} ∈ Fin)) |
3 | 1, 2 | mpbiri 257 |
. . . . 5
⊢ (𝑁 = {𝐼} → 𝑁 ∈ Fin) |
4 | 3 | adantr 481 |
. . . 4
⊢ ((𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) → 𝑁 ∈ Fin) |
5 | 4 | 3ad2ant2 1133 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) |
6 | | simp1 1135 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ CRing) |
7 | | simp3 1137 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ 𝐵) |
8 | | chpmat1d.c |
. . . 4
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
9 | | chpmat1d.a |
. . . 4
⊢ 𝐴 = (𝑁 Mat 𝑅) |
10 | | chpmat1d.b |
. . . 4
⊢ 𝐵 = (Base‘𝐴) |
11 | | chpmat1d.p |
. . . 4
⊢ 𝑃 = (Poly1‘𝑅) |
12 | | eqid 2738 |
. . . 4
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) |
13 | | eqid 2738 |
. . . 4
⊢ (𝑁 maDet 𝑃) = (𝑁 maDet 𝑃) |
14 | | eqid 2738 |
. . . 4
⊢
(-g‘(𝑁 Mat 𝑃)) = (-g‘(𝑁 Mat 𝑃)) |
15 | | eqid 2738 |
. . . 4
⊢
(var1‘𝑅) = (var1‘𝑅) |
16 | | eqid 2738 |
. . . 4
⊢ (
·𝑠 ‘(𝑁 Mat 𝑃)) = ( ·𝑠
‘(𝑁 Mat 𝑃)) |
17 | | eqid 2738 |
. . . 4
⊢ (𝑁 matToPolyMat 𝑅) = (𝑁 matToPolyMat 𝑅) |
18 | | eqid 2738 |
. . . 4
⊢
(1r‘(𝑁 Mat 𝑃)) = (1r‘(𝑁 Mat 𝑃)) |
19 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | chpmatval 21990 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = ((𝑁 maDet 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)))) |
20 | 5, 6, 7, 19 | syl3anc 1370 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = ((𝑁 maDet 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)))) |
21 | 11 | ply1crng 21379 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
22 | 21 | 3ad2ant1 1132 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ CRing) |
23 | | simp2 1136 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉)) |
24 | | crngring 19805 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
25 | 11 | ply1ring 21429 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring) |
27 | 26 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring) |
28 | 12 | matring 21602 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → (𝑁 Mat 𝑃) ∈ Ring) |
29 | 5, 27, 28 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑁 Mat 𝑃) ∈ Ring) |
30 | | ringgrp 19798 |
. . . . . 6
⊢ ((𝑁 Mat 𝑃) ∈ Ring → (𝑁 Mat 𝑃) ∈ Grp) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑁 Mat 𝑃) ∈ Grp) |
32 | 12 | matlmod 21588 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑃 ∈ Ring) → (𝑁 Mat 𝑃) ∈ LMod) |
33 | 5, 27, 32 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝑁 Mat 𝑃) ∈ LMod) |
34 | 24 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
35 | | eqid 2738 |
. . . . . . . . 9
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
36 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
37 | 15, 35, 36 | vr1cl 21398 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
38 | 34, 37 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (var1‘𝑅) ∈
(Base‘(Poly1‘𝑅))) |
39 | 35 | ply1crng 21379 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ CRing →
(Poly1‘𝑅)
∈ CRing) |
40 | 39 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Poly1‘𝑅) ∈ CRing) |
41 | 11 | oveq2i 7278 |
. . . . . . . . . . 11
⊢ (𝑁 Mat 𝑃) = (𝑁 Mat (Poly1‘𝑅)) |
42 | 41 | matsca2 21579 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ Fin ∧
(Poly1‘𝑅)
∈ CRing) → (Poly1‘𝑅) = (Scalar‘(𝑁 Mat 𝑃))) |
43 | 5, 40, 42 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Poly1‘𝑅) = (Scalar‘(𝑁 Mat 𝑃))) |
44 | 43 | eqcomd 2744 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Scalar‘(𝑁 Mat 𝑃)) = (Poly1‘𝑅)) |
45 | 44 | fveq2d 6770 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (Base‘(Scalar‘(𝑁 Mat 𝑃))) =
(Base‘(Poly1‘𝑅))) |
46 | 38, 45 | eleqtrrd 2842 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (var1‘𝑅) ∈
(Base‘(Scalar‘(𝑁 Mat 𝑃)))) |
47 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘(𝑁 Mat
𝑃)) = (Base‘(𝑁 Mat 𝑃)) |
48 | 47, 18 | ringidcl 19817 |
. . . . . . 7
⊢ ((𝑁 Mat 𝑃) ∈ Ring →
(1r‘(𝑁 Mat
𝑃)) ∈
(Base‘(𝑁 Mat 𝑃))) |
49 | 29, 48 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (1r‘(𝑁 Mat 𝑃)) ∈ (Base‘(𝑁 Mat 𝑃))) |
50 | | eqid 2738 |
. . . . . . 7
⊢
(Scalar‘(𝑁 Mat
𝑃)) = (Scalar‘(𝑁 Mat 𝑃)) |
51 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘(Scalar‘(𝑁 Mat 𝑃))) = (Base‘(Scalar‘(𝑁 Mat 𝑃))) |
52 | 47, 50, 16, 51 | lmodvscl 20150 |
. . . . . 6
⊢ (((𝑁 Mat 𝑃) ∈ LMod ∧
(var1‘𝑅)
∈ (Base‘(Scalar‘(𝑁 Mat 𝑃))) ∧ (1r‘(𝑁 Mat 𝑃)) ∈ (Base‘(𝑁 Mat 𝑃))) → ((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃))) ∈ (Base‘(𝑁 Mat 𝑃))) |
53 | 33, 46, 49, 52 | syl3anc 1370 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃))) ∈ (Base‘(𝑁 Mat 𝑃))) |
54 | 17, 9, 10, 11, 12 | mat2pmatbas 21885 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑁 matToPolyMat 𝑅)‘𝑀) ∈ (Base‘(𝑁 Mat 𝑃))) |
55 | 5, 34, 7, 54 | syl3anc 1370 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((𝑁 matToPolyMat 𝑅)‘𝑀) ∈ (Base‘(𝑁 Mat 𝑃))) |
56 | 47, 14 | grpsubcl 18665 |
. . . . 5
⊢ (((𝑁 Mat 𝑃) ∈ Grp ∧
((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃))) ∈ (Base‘(𝑁 Mat 𝑃)) ∧ ((𝑁 matToPolyMat 𝑅)‘𝑀) ∈ (Base‘(𝑁 Mat 𝑃))) → (((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)) ∈ (Base‘(𝑁 Mat 𝑃))) |
57 | 31, 53, 55, 56 | syl3anc 1370 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)) ∈ (Base‘(𝑁 Mat 𝑃))) |
58 | 13, 12, 47 | m1detdiag 21756 |
. . . 4
⊢ ((𝑃 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ (((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)) ∈ (Base‘(𝑁 Mat 𝑃))) → ((𝑁 maDet 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))) = (𝐼(((var1‘𝑅)( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼)) |
59 | 22, 23, 57, 58 | syl3anc 1370 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((𝑁 maDet 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))) = (𝐼(((var1‘𝑅)( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼)) |
60 | | chpmat1d.x |
. . . . . . . . 9
⊢ 𝑋 = (var1‘𝑅) |
61 | 60 | eqcomi 2747 |
. . . . . . . 8
⊢
(var1‘𝑅) = 𝑋 |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (var1‘𝑅) = 𝑋) |
63 | 62 | oveq1d 7282 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃))) = (𝑋( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))) |
64 | 63 | oveq1d 7282 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀)) = ((𝑋( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))) |
65 | 64 | oveqd 7284 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼(((var1‘𝑅)( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼) = (𝐼((𝑋( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼)) |
66 | | chpmat1d.z |
. . . . . 6
⊢ − =
(-g‘𝑃) |
67 | | chpmat1d.s |
. . . . . 6
⊢ 𝑆 = (algSc‘𝑃) |
68 | 8, 11, 9, 10, 60, 66, 67, 12, 17 | chpmat1dlem 21994 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼((𝑋( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) |
69 | 24, 68 | syl3an1 1162 |
. . . 4
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼((𝑋( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) |
70 | 65, 69 | eqtrd 2778 |
. . 3
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼(((var1‘𝑅)( ·𝑠
‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) |
71 | 59, 70 | eqtrd 2778 |
. 2
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → ((𝑁 maDet 𝑃)‘(((var1‘𝑅)(
·𝑠 ‘(𝑁 Mat 𝑃))(1r‘(𝑁 Mat 𝑃)))(-g‘(𝑁 Mat 𝑃))((𝑁 matToPolyMat 𝑅)‘𝑀))) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) |
72 | 20, 71 | eqtrd 2778 |
1
⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) |