Metamath Proof Explorer

Theorem chpmat1d

Description: The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019)

Ref Expression
Hypotheses chpmat1d.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chpmat1d.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
chpmat1d.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
chpmat1d.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
chpmat1d.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
chpmat1d.z ⊢ − = ( -g ‘ 𝑃 )
chpmat1d.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
Assertion chpmat1d ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )

Proof

Step Hyp Ref Expression
1 chpmat1d.c ⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
2 chpmat1d.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 chpmat1d.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4 chpmat1d.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
5 chpmat1d.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
6 chpmat1d.z ⊢ − = ( -g ‘ 𝑃 )
7 chpmat1d.s ⊢ 𝑆 = ( algSc ‘ 𝑃 )
8 snfi ⊢ { 𝐼 } ∈ Fin
9 eleq1 ⊢ ( 𝑁 = { 𝐼 } → ( 𝑁 ∈ Fin ↔ { 𝐼 } ∈ Fin ) )
10 8 9 mpbiri ⊢ ( 𝑁 = { 𝐼 } → 𝑁 ∈ Fin )
11 10 adantr ⊢ ( ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) → 𝑁 ∈ Fin )
12 11 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
13 simp1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ CRing )
14 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
15 eqid ⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
16 eqid ⊢ ( 𝑁 maDet 𝑃 ) = ( 𝑁 maDet 𝑃 )
17 eqid ⊢ ( -g ‘ ( 𝑁 Mat 𝑃 ) ) = ( -g ‘ ( 𝑁 Mat 𝑃 ) )
18 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
19 eqid ⊢ ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) )
20 eqid ⊢ ( 𝑁 matToPolyMat 𝑅 ) = ( 𝑁 matToPolyMat 𝑅 )
21 eqid ⊢ ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
22 1 3 4 2 15 16 17 18 19 20 21 chpmatval ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) )
23 12 13 14 22 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( ( 𝑁 maDet 𝑃 ) ‘ ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) )
24 2 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
25 24 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ CRing )
26 simp2 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) )
27 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
28 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
29 27 28 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
30 29 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
31 15 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( 𝑁 Mat 𝑃 ) ∈ Ring )
32 12 30 31 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 Mat 𝑃 ) ∈ Ring )
33 ringgrp ⊢ ( ( 𝑁 Mat 𝑃 ) ∈ Ring → ( 𝑁 Mat 𝑃 ) ∈ Grp )
34 32 33 syl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 Mat 𝑃 ) ∈ Grp )
35 15 matlmod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( 𝑁 Mat 𝑃 ) ∈ LMod )
36 12 30 35 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 Mat 𝑃 ) ∈ LMod )
37 27 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
38 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
39 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
40 18 38 39 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
41 37 40 syl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
42 38 ply1crng ⊢ ( 𝑅 ∈ CRing → ( Poly1 ‘ 𝑅 ) ∈ CRing )
43 42 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Poly1 ‘ 𝑅 ) ∈ CRing )
44 2 oveq2i ⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat ( Poly1 ‘ 𝑅 ) )
45 44 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ ( Poly1 ‘ 𝑅 ) ∈ CRing ) → ( Poly1 ‘ 𝑅 ) = ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) )
46 12 43 45 syl2anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Poly1 ‘ 𝑅 ) = ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) )
47 46 eqcomd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) = ( Poly1 ‘ 𝑅 ) )
48 47 fveq2d ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
49 41 48 eleqtrrd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) ) )
50 eqid ⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
51 50 21 ringidcl ⊢ ( ( 𝑁 Mat 𝑃 ) ∈ Ring → ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
52 32 51 syl ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
53 eqid ⊢ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) = ( Scalar ‘ ( 𝑁 Mat 𝑃 ) )
54 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) )
55 50 53 19 54 lmodvscl ⊢ ( ( ( 𝑁 Mat 𝑃 ) ∈ LMod ∧ ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Scalar ‘ ( 𝑁 Mat 𝑃 ) ) ) ∧ ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) → ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
56 36 49 52 55 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
57 20 3 4 2 15 mat2pmatbas ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
58 12 37 14 57 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
59 50 17 grpsubcl ⊢ ( ( ( 𝑁 Mat 𝑃 ) ∈ Grp ∧ ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ∧ ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) ) → ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
60 34 56 58 59 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ∈ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) )
61 16 15 50 m1detdiag ⊢ ( ( 𝑃 ∈ 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 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) )
62 25 26 60 61 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝐼 ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) )
63 5 eqcomi ⊢ ( var1 ‘ 𝑅 ) = 𝑋
64 63 a1i ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( var1 ‘ 𝑅 ) = 𝑋 )
65 64 oveq1d ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) = ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) )
66 65 oveq1d ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) = ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) )
67 66 oveqd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) = ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) )
68 1 2 3 4 5 6 7 15 20 chpmat1dlem ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )
69 27 68 syl3an1 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( 𝑋 ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )
70 67 69 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐼 ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) 𝐼 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )
71 62 70 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 maDet 𝑃 ) ‘ ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ ( 𝑁 Mat 𝑃 ) ) ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) ) ( -g ‘ ( 𝑁 Mat 𝑃 ) ) ( ( 𝑁 matToPolyMat 𝑅 ) ‘ 𝑀 ) ) ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )
72 23 71 eqtrd ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑁 = { 𝐼 } ∧ 𝐼 ∈ 𝑉 ) ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) = ( 𝑋 − ( 𝑆 ‘ ( 𝐼 𝑀 𝐼 ) ) ) )