Proof of Theorem chpmat0d
Step | Hyp | Ref
| Expression |
1 | | 0fin 8919 |
. . 3
⊢ ∅
∈ Fin |
2 | | id 22 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
3 | | 0ex 5234 |
. . . . 5
⊢ ∅
∈ V |
4 | 3 | snid 4602 |
. . . 4
⊢ ∅
∈ {∅} |
5 | | mat0dimbas0 21596 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat 𝑅)) = {∅}) |
6 | 4, 5 | eleqtrrid 2847 |
. . 3
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat 𝑅))) |
7 | | chpmat0.c |
. . . 4
⊢ 𝐶 = (∅ CharPlyMat 𝑅) |
8 | | eqid 2739 |
. . . 4
⊢ (∅
Mat 𝑅) = (∅ Mat 𝑅) |
9 | | eqid 2739 |
. . . 4
⊢
(Base‘(∅ Mat 𝑅)) = (Base‘(∅ Mat 𝑅)) |
10 | | eqid 2739 |
. . . 4
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
11 | | eqid 2739 |
. . . 4
⊢ (∅
Mat (Poly1‘𝑅)) = (∅ Mat
(Poly1‘𝑅)) |
12 | | eqid 2739 |
. . . 4
⊢ (∅
maDet (Poly1‘𝑅)) = (∅ maDet
(Poly1‘𝑅)) |
13 | | eqid 2739 |
. . . 4
⊢
(-g‘(∅ Mat (Poly1‘𝑅))) =
(-g‘(∅ Mat (Poly1‘𝑅))) |
14 | | eqid 2739 |
. . . 4
⊢
(var1‘𝑅) = (var1‘𝑅) |
15 | | eqid 2739 |
. . . 4
⊢ (
·𝑠 ‘(∅ Mat
(Poly1‘𝑅))) = ( ·𝑠
‘(∅ Mat (Poly1‘𝑅))) |
16 | | eqid 2739 |
. . . 4
⊢ (∅
matToPolyMat 𝑅) = (∅
matToPolyMat 𝑅) |
17 | | eqid 2739 |
. . . 4
⊢
(1r‘(∅ Mat (Poly1‘𝑅))) =
(1r‘(∅ Mat (Poly1‘𝑅))) |
18 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 | chpmatval 21961 |
. . 3
⊢ ((∅
∈ Fin ∧ 𝑅 ∈
Ring ∧ ∅ ∈ (Base‘(∅ Mat 𝑅))) → (𝐶‘∅) = ((∅ maDet
(Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
19 | 1, 2, 6, 18 | mp3an2i 1464 |
. 2
⊢ (𝑅 ∈ Ring → (𝐶‘∅) = ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
20 | 10 | ply1ring 21400 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Poly1‘𝑅)
∈ Ring) |
21 | | mdet0pr 21722 |
. . . . 5
⊢
((Poly1‘𝑅) ∈ Ring → (∅ maDet
(Poly1‘𝑅))
= {〈∅, (1r‘(Poly1‘𝑅))〉}) |
22 | 21 | fveq1d 6770 |
. . . 4
⊢
((Poly1‘𝑅) ∈ Ring → ((∅ maDet
(Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
23 | 20, 22 | syl 17 |
. . 3
⊢ (𝑅 ∈ Ring → ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
24 | 11 | mat0dimid 21598 |
. . . . . . . . . 10
⊢
((Poly1‘𝑅) ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
25 | 20, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
26 | 25 | oveq2d 7284 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅)) |
27 | | eqid 2739 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
28 | 14, 10, 27 | vr1cl 21369 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
29 | 11 | mat0dimscm 21599 |
. . . . . . . . 9
⊢
(((Poly1‘𝑅) ∈ Ring ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) → ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
30 | 20, 28, 29 | syl2anc 583 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
31 | 26, 30 | eqtrd 2779 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ∅) |
32 | | d0mat2pmat 21868 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ((∅
matToPolyMat 𝑅)‘∅) = ∅) |
33 | 31, 32 | oveq12d 7286 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅)) |
34 | 11 | matring 21573 |
. . . . . . . . 9
⊢ ((∅
∈ Fin ∧ (Poly1‘𝑅) ∈ Ring) → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
35 | 1, 20, 34 | sylancr 586 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
36 | | ringgrp 19769 |
. . . . . . . 8
⊢ ((∅
Mat (Poly1‘𝑅)) ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
38 | | mat0dimbas0 21596 |
. . . . . . . . 9
⊢
((Poly1‘𝑅) ∈ Ring → (Base‘(∅
Mat (Poly1‘𝑅))) = {∅}) |
39 | 20, 38 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat (Poly1‘𝑅))) = {∅}) |
40 | 4, 39 | eleqtrrid 2847 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat (Poly1‘𝑅)))) |
41 | | eqid 2739 |
. . . . . . . 8
⊢
(Base‘(∅ Mat (Poly1‘𝑅))) = (Base‘(∅ Mat
(Poly1‘𝑅))) |
42 | | eqid 2739 |
. . . . . . . 8
⊢
(0g‘(∅ Mat (Poly1‘𝑅))) =
(0g‘(∅ Mat (Poly1‘𝑅))) |
43 | 41, 42, 13 | grpsubid 18640 |
. . . . . . 7
⊢
(((∅ Mat (Poly1‘𝑅)) ∈ Grp ∧ ∅ ∈
(Base‘(∅ Mat (Poly1‘𝑅)))) →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
44 | 37, 40, 43 | syl2anc 583 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
45 | 33, 44 | eqtrd 2779 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
46 | 45 | fveq2d 6772 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅))))) |
47 | 11 | mat0dim0 21597 |
. . . . . . 7
⊢
((Poly1‘𝑅) ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
48 | 20, 47 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
49 | 48 | fveq2d 6772 |
. . . . 5
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘∅)) |
50 | | fvex 6781 |
. . . . . 6
⊢
(1r‘(Poly1‘𝑅)) ∈ V |
51 | 3, 50 | fvsn 7047 |
. . . . 5
⊢
({〈∅, (1r‘(Poly1‘𝑅))〉}‘∅) =
(1r‘(Poly1‘𝑅)) |
52 | 49, 51 | eqtrdi 2795 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) =
(1r‘(Poly1‘𝑅))) |
53 | 46, 52 | eqtrd 2779 |
. . 3
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
54 | 23, 53 | eqtrd 2779 |
. 2
⊢ (𝑅 ∈ Ring → ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
55 | 19, 54 | eqtrd 2779 |
1
⊢ (𝑅 ∈ Ring → (𝐶‘∅) =
(1r‘(Poly1‘𝑅))) |