Metamath Proof Explorer


Theorem cayleyhamiltonALT

Description: Alternate proof of cayleyhamilton , the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 directly, but has the same structure as the proof of cayleyhamilton0 . In contrast to the proof of cayleyhamilton0 , only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses cayleyhamilton.a A=NMatR
cayleyhamilton.b B=BaseA
cayleyhamilton.0 0˙=0A
cayleyhamilton.c C=NCharPlyMatR
cayleyhamilton.k K=coe1CM
cayleyhamilton.m ˙=A
cayleyhamilton.e ×˙=mulGrpA
Assertion cayleyhamiltonALT NFinRCRingMBAn0Kn˙n×˙M=0˙

Proof

Step Hyp Ref Expression
1 cayleyhamilton.a A=NMatR
2 cayleyhamilton.b B=BaseA
3 cayleyhamilton.0 0˙=0A
4 cayleyhamilton.c C=NCharPlyMatR
5 cayleyhamilton.k K=coe1CM
6 cayleyhamilton.m ˙=A
7 cayleyhamilton.e ×˙=mulGrpA
8 eqid Poly1R=Poly1R
9 eqid NMatPoly1R=NMatPoly1R
10 eqid NMatPoly1R=NMatPoly1R
11 eqid -NMatPoly1R=-NMatPoly1R
12 eqid 0NMatPoly1R=0NMatPoly1R
13 eqid NmatToPolyMatR=NmatToPolyMatR
14 eqid CM=CM
15 eqeq1 l=nl=0n=0
16 eqeq1 l=nl=s+1n=s+1
17 breq2 l=ns+1<ls+1<n
18 oveq1 l=nl1=n1
19 18 fveq2d l=nbl1=bn1
20 19 fveq2d l=nNmatToPolyMatRbl1=NmatToPolyMatRbn1
21 fveq2 l=nbl=bn
22 21 fveq2d l=nNmatToPolyMatRbl=NmatToPolyMatRbn
23 22 oveq2d l=nNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=NmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
24 20 23 oveq12d l=nNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=NmatToPolyMatRbn1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
25 17 24 ifbieq2d l=nifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=ifs+1<n0NMatPoly1RNmatToPolyMatRbn1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
26 16 25 ifbieq2d l=nifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=ifn=s+1NmatToPolyMatRbsifs+1<n0NMatPoly1RNmatToPolyMatRbn1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
27 15 26 ifbieq2d l=nifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=ifn=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifn=s+1NmatToPolyMatRbsifs+1<n0NMatPoly1RNmatToPolyMatRbn1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
28 27 cbvmptv l0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbl=n0ifn=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifn=s+1NmatToPolyMatRbsifs+1<n0NMatPoly1RNmatToPolyMatRbn1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbn
29 eqid BaseNMatPoly1R=BaseNMatPoly1R
30 eqid 1A=1A
31 eqid NcPolyMatToMatR=NcPolyMatToMatR
32 eqid mulGrpNMatPoly1R=mulGrpNMatPoly1R
33 1 2 8 9 10 11 12 13 4 14 28 29 30 6 31 7 32 cayhamlem4 NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=NcPolyMatToMatRNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
34 eqid NConstPolyMatR=NConstPolyMatR
35 31 34 cpm2mfval NFinRCRingNcPolyMatToMatR=mNConstPolyMatRxN,yNcoe1xmy0
36 35 eqcomd NFinRCRingmNConstPolyMatRxN,yNcoe1xmy0=NcPolyMatToMatR
37 36 3adant3 NFinRCRingMBmNConstPolyMatRxN,yNcoe1xmy0=NcPolyMatToMatR
38 37 fveq1d NFinRCRingMBmNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=NcPolyMatToMatRNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
39 38 eqeq2d NFinRCRingMBAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0coe1CMn˙n×˙M=NcPolyMatToMatRNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
40 39 2rexbidv NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnsbB0sAn0coe1CMn˙n×˙M=NcPolyMatToMatRNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
41 33 40 mpbird NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
42 5 eqcomi coe1CM=K
43 42 a1i NFinRCRingMBsbB0sn0coe1CM=K
44 43 fveq1d NFinRCRingMBsbB0sn0coe1CMn=Kn
45 44 oveq1d NFinRCRingMBsbB0sn0coe1CMn˙n×˙M=Kn˙n×˙M
46 45 mpteq2dva NFinRCRingMBsbB0sn0coe1CMn˙n×˙M=n0Kn˙n×˙M
47 46 oveq2d NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=An0Kn˙n×˙M
48 47 eqeq1d NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0Kn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
49 48 biimpa NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0Kn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln
50 oveq1 n=jnmulGrpNMatPoly1RNmatToPolyMatRM=jmulGrpNMatPoly1RNmatToPolyMatRM
51 fveq2 n=jl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=l0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj
52 50 51 oveq12d n=jnmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=jmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj
53 52 cbvmptv n0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=j0jmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj
54 53 oveq2i NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=NMatPoly1Rj0jmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj
55 54 a1i NFinRCRingMBsbB0sNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=NMatPoly1Rj0jmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj
56 1 2 8 9 10 11 12 13 28 32 cayhamlem1 NFinRCRingMBsbB0sNMatPoly1Rj0jmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblj=0NMatPoly1R
57 55 56 eqtrd NFinRCRingMBsbB0sNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0NMatPoly1R
58 fveq2 NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0NMatPoly1RmNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=mNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R
59 crngring RCRingRRing
60 59 anim2i NFinRCRingNFinRRing
61 60 3adant3 NFinRCRingMBNFinRRing
62 31 34 cpm2mfval NFinRRingNcPolyMatToMatR=mNConstPolyMatRxN,yNcoe1xmy0
63 62 eqcomd NFinRRingmNConstPolyMatRxN,yNcoe1xmy0=NcPolyMatToMatR
64 63 fveq1d NFinRRingmNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R=NcPolyMatToMatR0NMatPoly1R
65 eqid 0A=0A
66 1 31 8 9 65 12 m2cpminv0 NFinRRingNcPolyMatToMatR0NMatPoly1R=0A
67 64 66 eqtrd NFinRRingmNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R=0A
68 61 67 syl NFinRCRingMBmNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R=0A
69 68 3 eqtr4di NFinRCRingMBmNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R=0˙
70 69 adantr NFinRCRingMBsbB0smNConstPolyMatRxN,yNcoe1xmy00NMatPoly1R=0˙
71 58 70 sylan9eqr NFinRCRingMBsbB0sNMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0NMatPoly1RmNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0˙
72 57 71 mpdan NFinRCRingMBsbB0smNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0˙
73 72 adantr NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnmNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRbln=0˙
74 49 73 eqtrd NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0Kn˙n×˙M=0˙
75 74 ex NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0Kn˙n×˙M=0˙
76 75 rexlimdvva NFinRCRingMBsbB0sAn0coe1CMn˙n×˙M=mNConstPolyMatRxN,yNcoe1xmy0NMatPoly1Rn0nmulGrpNMatPoly1RNmatToPolyMatRMNMatPoly1Rl0ifl=00NMatPoly1R-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRb0ifl=s+1NmatToPolyMatRbsifs+1<l0NMatPoly1RNmatToPolyMatRbl1-NMatPoly1RNmatToPolyMatRMNMatPoly1RNmatToPolyMatRblnAn0Kn˙n×˙M=0˙
77 41 76 mpd NFinRCRingMBAn0Kn˙n×˙M=0˙