Proof of Theorem chpmat0d
| Step | Hyp | Ref
| Expression |
| 1 | | 0fi 9082 |
. . 3
⊢ ∅
∈ Fin |
| 2 | | id 22 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
| 3 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 4 | 3 | snid 4662 |
. . . 4
⊢ ∅
∈ {∅} |
| 5 | | mat0dimbas0 22472 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat 𝑅)) = {∅}) |
| 6 | 4, 5 | eleqtrrid 2848 |
. . 3
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat 𝑅))) |
| 7 | | chpmat0.c |
. . . 4
⊢ 𝐶 = (∅ CharPlyMat 𝑅) |
| 8 | | eqid 2737 |
. . . 4
⊢ (∅
Mat 𝑅) = (∅ Mat 𝑅) |
| 9 | | eqid 2737 |
. . . 4
⊢
(Base‘(∅ Mat 𝑅)) = (Base‘(∅ Mat 𝑅)) |
| 10 | | eqid 2737 |
. . . 4
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
| 11 | | eqid 2737 |
. . . 4
⊢ (∅
Mat (Poly1‘𝑅)) = (∅ Mat
(Poly1‘𝑅)) |
| 12 | | eqid 2737 |
. . . 4
⊢ (∅
maDet (Poly1‘𝑅)) = (∅ maDet
(Poly1‘𝑅)) |
| 13 | | eqid 2737 |
. . . 4
⊢
(-g‘(∅ Mat (Poly1‘𝑅))) =
(-g‘(∅ Mat (Poly1‘𝑅))) |
| 14 | | eqid 2737 |
. . . 4
⊢
(var1‘𝑅) = (var1‘𝑅) |
| 15 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘(∅ Mat
(Poly1‘𝑅))) = ( ·𝑠
‘(∅ Mat (Poly1‘𝑅))) |
| 16 | | eqid 2737 |
. . . 4
⊢ (∅
matToPolyMat 𝑅) = (∅
matToPolyMat 𝑅) |
| 17 | | eqid 2737 |
. . . 4
⊢
(1r‘(∅ Mat (Poly1‘𝑅))) =
(1r‘(∅ Mat (Poly1‘𝑅))) |
| 18 | 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17 | chpmatval 22837 |
. . 3
⊢ ((∅
∈ Fin ∧ 𝑅 ∈
Ring ∧ ∅ ∈ (Base‘(∅ Mat 𝑅))) → (𝐶‘∅) = ((∅ maDet
(Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
| 19 | 1, 2, 6, 18 | mp3an2i 1468 |
. 2
⊢ (𝑅 ∈ Ring → (𝐶‘∅) = ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
| 20 | 10 | ply1ring 22249 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Poly1‘𝑅)
∈ Ring) |
| 21 | | mdet0pr 22598 |
. . . . 5
⊢
((Poly1‘𝑅) ∈ Ring → (∅ maDet
(Poly1‘𝑅))
= {〈∅, (1r‘(Poly1‘𝑅))〉}) |
| 22 | 21 | fveq1d 6908 |
. . . 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 22474 |
. . . . . . . . . 10
⊢
((Poly1‘𝑅) ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
| 25 | 20, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
| 26 | 25 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅)) |
| 27 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
| 28 | 14, 10, 27 | vr1cl 22219 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
| 29 | 11 | mat0dimscm 22475 |
. . . . . . . . 9
⊢
(((Poly1‘𝑅) ∈ Ring ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) → ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
| 30 | 20, 28, 29 | syl2anc 584 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
| 31 | 26, 30 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ∅) |
| 32 | | d0mat2pmat 22744 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ((∅
matToPolyMat 𝑅)‘∅) = ∅) |
| 33 | 31, 32 | oveq12d 7449 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅)) |
| 34 | 11 | matring 22449 |
. . . . . . . . 9
⊢ ((∅
∈ Fin ∧ (Poly1‘𝑅) ∈ Ring) → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
| 35 | 1, 20, 34 | sylancr 587 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
| 36 | | ringgrp 20235 |
. . . . . . . 8
⊢ ((∅
Mat (Poly1‘𝑅)) ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
| 37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
| 38 | | mat0dimbas0 22472 |
. . . . . . . . 9
⊢
((Poly1‘𝑅) ∈ Ring → (Base‘(∅
Mat (Poly1‘𝑅))) = {∅}) |
| 39 | 20, 38 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat (Poly1‘𝑅))) = {∅}) |
| 40 | 4, 39 | eleqtrrid 2848 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat (Poly1‘𝑅)))) |
| 41 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(∅ Mat (Poly1‘𝑅))) = (Base‘(∅ Mat
(Poly1‘𝑅))) |
| 42 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘(∅ Mat (Poly1‘𝑅))) =
(0g‘(∅ Mat (Poly1‘𝑅))) |
| 43 | 41, 42, 13 | grpsubid 19042 |
. . . . . . 7
⊢
(((∅ Mat (Poly1‘𝑅)) ∈ Grp ∧ ∅ ∈
(Base‘(∅ Mat (Poly1‘𝑅)))) →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
| 44 | 37, 40, 43 | syl2anc 584 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
| 45 | 33, 44 | eqtrd 2777 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
| 46 | 45 | fveq2d 6910 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅))))) |
| 47 | 11 | mat0dim0 22473 |
. . . . . . 7
⊢
((Poly1‘𝑅) ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
| 48 | 20, 47 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
| 49 | 48 | fveq2d 6910 |
. . . . 5
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘∅)) |
| 50 | | fvex 6919 |
. . . . . 6
⊢
(1r‘(Poly1‘𝑅)) ∈ V |
| 51 | 3, 50 | fvsn 7201 |
. . . . 5
⊢
({〈∅, (1r‘(Poly1‘𝑅))〉}‘∅) =
(1r‘(Poly1‘𝑅)) |
| 52 | 49, 51 | eqtrdi 2793 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) =
(1r‘(Poly1‘𝑅))) |
| 53 | 46, 52 | eqtrd 2777 |
. . 3
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
| 54 | 23, 53 | eqtrd 2777 |
. 2
⊢ (𝑅 ∈ Ring → ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
| 55 | 19, 54 | eqtrd 2777 |
1
⊢ (𝑅 ∈ Ring → (𝐶‘∅) =
(1r‘(Poly1‘𝑅))) |