Proof of Theorem chpmat0d
Step | Hyp | Ref
| Expression |
1 | | 0fin 8476 |
. . . 4
⊢ ∅
∈ Fin |
2 | 1 | a1i 11 |
. . 3
⊢ (𝑅 ∈ Ring → ∅
∈ Fin) |
3 | | id 22 |
. . 3
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Ring) |
4 | | 0ex 5026 |
. . . . 5
⊢ ∅
∈ V |
5 | 4 | snid 4430 |
. . . 4
⊢ ∅
∈ {∅} |
6 | | mat0dimbas0 20677 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat 𝑅)) = {∅}) |
7 | 5, 6 | syl5eleqr 2866 |
. . 3
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat 𝑅))) |
8 | | chpmat0.c |
. . . 4
⊢ 𝐶 = (∅ CharPlyMat 𝑅) |
9 | | eqid 2778 |
. . . 4
⊢ (∅
Mat 𝑅) = (∅ Mat 𝑅) |
10 | | eqid 2778 |
. . . 4
⊢
(Base‘(∅ Mat 𝑅)) = (Base‘(∅ Mat 𝑅)) |
11 | | eqid 2778 |
. . . 4
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
12 | | eqid 2778 |
. . . 4
⊢ (∅
Mat (Poly1‘𝑅)) = (∅ Mat
(Poly1‘𝑅)) |
13 | | eqid 2778 |
. . . 4
⊢ (∅
maDet (Poly1‘𝑅)) = (∅ maDet
(Poly1‘𝑅)) |
14 | | eqid 2778 |
. . . 4
⊢
(-g‘(∅ Mat (Poly1‘𝑅))) =
(-g‘(∅ Mat (Poly1‘𝑅))) |
15 | | eqid 2778 |
. . . 4
⊢
(var1‘𝑅) = (var1‘𝑅) |
16 | | eqid 2778 |
. . . 4
⊢ (
·𝑠 ‘(∅ Mat
(Poly1‘𝑅))) = ( ·𝑠
‘(∅ Mat (Poly1‘𝑅))) |
17 | | eqid 2778 |
. . . 4
⊢ (∅
matToPolyMat 𝑅) = (∅
matToPolyMat 𝑅) |
18 | | eqid 2778 |
. . . 4
⊢
(1r‘(∅ Mat (Poly1‘𝑅))) =
(1r‘(∅ Mat (Poly1‘𝑅))) |
19 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | chpmatval 21043 |
. . 3
⊢ ((∅
∈ Fin ∧ 𝑅 ∈
Ring ∧ ∅ ∈ (Base‘(∅ Mat 𝑅))) → (𝐶‘∅) = ((∅ maDet
(Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
20 | 2, 3, 7, 19 | syl3anc 1439 |
. 2
⊢ (𝑅 ∈ Ring → (𝐶‘∅) = ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)))) |
21 | 11 | ply1ring 20014 |
. . . 4
⊢ (𝑅 ∈ Ring →
(Poly1‘𝑅)
∈ Ring) |
22 | | mdet0pr 20803 |
. . . . 5
⊢
((Poly1‘𝑅) ∈ Ring → (∅ maDet
(Poly1‘𝑅))
= {〈∅, (1r‘(Poly1‘𝑅))〉}) |
23 | 22 | fveq1d 6448 |
. . . 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 𝑅)‘∅)))) |
24 | 21, 23 | 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 𝑅)‘∅)))) |
25 | 12 | mat0dimid 20679 |
. . . . . . . . . 10
⊢
((Poly1‘𝑅) ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
26 | 21, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(1r‘(∅ Mat (Poly1‘𝑅))) = ∅) |
27 | 26 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅)) |
28 | | eqid 2778 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
29 | 15, 11, 28 | vr1cl 19983 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) |
30 | 12 | mat0dimscm 20680 |
. . . . . . . . 9
⊢
(((Poly1‘𝑅) ∈ Ring ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑅))) → ((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
31 | 21, 29, 30 | syl2anc 579 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))∅) = ∅) |
32 | 27, 31 | eqtrd 2814 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅)))) = ∅) |
33 | | d0mat2pmat 20950 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ((∅
matToPolyMat 𝑅)‘∅) = ∅) |
34 | 32, 33 | oveq12d 6940 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅)) |
35 | 12 | matring 20653 |
. . . . . . . . 9
⊢ ((∅
∈ Fin ∧ (Poly1‘𝑅) ∈ Ring) → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
36 | 1, 21, 35 | sylancr 581 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Ring) |
37 | | ringgrp 18939 |
. . . . . . . 8
⊢ ((∅
Mat (Poly1‘𝑅)) ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → (∅ Mat
(Poly1‘𝑅))
∈ Grp) |
39 | | mat0dimbas0 20677 |
. . . . . . . . 9
⊢
((Poly1‘𝑅) ∈ Ring → (Base‘(∅
Mat (Poly1‘𝑅))) = {∅}) |
40 | 21, 39 | syl 17 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(Base‘(∅ Mat (Poly1‘𝑅))) = {∅}) |
41 | 5, 40 | syl5eleqr 2866 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → ∅
∈ (Base‘(∅ Mat (Poly1‘𝑅)))) |
42 | | eqid 2778 |
. . . . . . . 8
⊢
(Base‘(∅ Mat (Poly1‘𝑅))) = (Base‘(∅ Mat
(Poly1‘𝑅))) |
43 | | eqid 2778 |
. . . . . . . 8
⊢
(0g‘(∅ Mat (Poly1‘𝑅))) =
(0g‘(∅ Mat (Poly1‘𝑅))) |
44 | 42, 43, 14 | grpsubid 17886 |
. . . . . . 7
⊢
(((∅ Mat (Poly1‘𝑅)) ∈ Grp ∧ ∅ ∈
(Base‘(∅ Mat (Poly1‘𝑅)))) →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
45 | 38, 41, 44 | syl2anc 579 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∅(-g‘(∅ Mat (Poly1‘𝑅)))∅) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
46 | 34, 45 | eqtrd 2814 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((var1‘𝑅)( ·𝑠
‘(∅ Mat (Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅)) =
(0g‘(∅ Mat (Poly1‘𝑅)))) |
47 | 46 | fveq2d 6450 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅))))) |
48 | 12 | mat0dim0 20678 |
. . . . . . 7
⊢
((Poly1‘𝑅) ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
49 | 21, 48 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(0g‘(∅ Mat (Poly1‘𝑅))) = ∅) |
50 | 49 | fveq2d 6450 |
. . . . 5
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) = ({〈∅,
(1r‘(Poly1‘𝑅))〉}‘∅)) |
51 | | fvex 6459 |
. . . . . 6
⊢
(1r‘(Poly1‘𝑅)) ∈ V |
52 | 4, 51 | fvsn 6714 |
. . . . 5
⊢
({〈∅, (1r‘(Poly1‘𝑅))〉}‘∅) =
(1r‘(Poly1‘𝑅)) |
53 | 50, 52 | syl6eq 2830 |
. . . 4
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(0g‘(∅
Mat (Poly1‘𝑅)))) =
(1r‘(Poly1‘𝑅))) |
54 | 47, 53 | eqtrd 2814 |
. . 3
⊢ (𝑅 ∈ Ring →
({〈∅, (1r‘(Poly1‘𝑅))〉}‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
55 | 24, 54 | eqtrd 2814 |
. 2
⊢ (𝑅 ∈ Ring → ((∅
maDet (Poly1‘𝑅))‘(((var1‘𝑅)(
·𝑠 ‘(∅ Mat
(Poly1‘𝑅)))(1r‘(∅ Mat
(Poly1‘𝑅))))(-g‘(∅ Mat
(Poly1‘𝑅)))((∅ matToPolyMat 𝑅)‘∅))) =
(1r‘(Poly1‘𝑅))) |
56 | 20, 55 | eqtrd 2814 |
1
⊢ (𝑅 ∈ Ring → (𝐶‘∅) =
(1r‘(Poly1‘𝑅))) |