Metamath Proof Explorer


Theorem pm2mpmhmlem1

Description: Lemma 1 for pm2mpmhm . (Contributed by AV, 21-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p P=Poly1R
pm2mpfo.c C=NMatP
pm2mpfo.b B=BaseC
pm2mpfo.m ˙=Q
pm2mpfo.e ×˙=mulGrpQ
pm2mpfo.x X=var1A
pm2mpfo.a A=NMatR
pm2mpfo.q Q=Poly1A
pm2mpfo.l L=BaseQ
pm2mpfo.t T=NpMatToMatPolyR
Assertion pm2mpmhmlem1 NFinRRingxByBfinSupp0Ql0Ak=0lxdecompPMatkAydecompPMatlk˙l×˙X

Proof

Step Hyp Ref Expression
1 pm2mpfo.p P=Poly1R
2 pm2mpfo.c C=NMatP
3 pm2mpfo.b B=BaseC
4 pm2mpfo.m ˙=Q
5 pm2mpfo.e ×˙=mulGrpQ
6 pm2mpfo.x X=var1A
7 pm2mpfo.a A=NMatR
8 pm2mpfo.q Q=Poly1A
9 pm2mpfo.l L=BaseQ
10 pm2mpfo.t T=NpMatToMatPolyR
11 fvexd NFinRRingxByB0QV
12 ovexd NFinRRingxByBl0Ak=0lxdecompPMatkAydecompPMatlk˙l×˙XV
13 oveq2 l=n0l=0n
14 oveq1 l=nlk=nk
15 14 oveq2d l=nydecompPMatlk=ydecompPMatnk
16 15 oveq2d l=nxdecompPMatkAydecompPMatlk=xdecompPMatkAydecompPMatnk
17 13 16 mpteq12dv l=nk0lxdecompPMatkAydecompPMatlk=k0nxdecompPMatkAydecompPMatnk
18 17 oveq2d l=nAk=0lxdecompPMatkAydecompPMatlk=Ak=0nxdecompPMatkAydecompPMatnk
19 oveq1 l=nl×˙X=n×˙X
20 18 19 oveq12d l=nAk=0lxdecompPMatkAydecompPMatlk˙l×˙X=Ak=0nxdecompPMatkAydecompPMatnk˙n×˙X
21 simpll NFinRRingxByBNFin
22 simplr NFinRRingxByBRRing
23 1 2 pmatring NFinRRingCRing
24 23 anim1i NFinRRingxByBCRingxByB
25 3anass CRingxByBCRingxByB
26 24 25 sylibr NFinRRingxByBCRingxByB
27 eqid C=C
28 3 27 ringcl CRingxByBxCyB
29 26 28 syl NFinRRingxByBxCyB
30 eqid 0R=0R
31 1 2 3 30 pmatcoe1fsupp NFinRRingxCyBs0n0s<naNbNcoe1axCybn=0R
32 21 22 29 31 syl3anc NFinRRingxByBs0n0s<naNbNcoe1axCybn=0R
33 fvoveq1 a=icoe1axCyb=coe1ixCyb
34 33 fveq1d a=icoe1axCybn=coe1ixCybn
35 34 eqeq1d a=icoe1axCybn=0Rcoe1ixCybn=0R
36 oveq2 b=jixCyb=ixCyj
37 36 fveq2d b=jcoe1ixCyb=coe1ixCyj
38 37 fveq1d b=jcoe1ixCybn=coe1ixCyjn
39 38 eqeq1d b=jcoe1ixCybn=0Rcoe1ixCyjn=0R
40 35 39 rspc2va iNjNaNbNcoe1axCybn=0Rcoe1ixCyjn=0R
41 40 expcom aNbNcoe1axCybn=0RiNjNcoe1ixCyjn=0R
42 41 adantl NFinRRingxByBn0aNbNcoe1axCybn=0RiNjNcoe1ixCyjn=0R
43 42 3impib NFinRRingxByBn0aNbNcoe1axCybn=0RiNjNcoe1ixCyjn=0R
44 43 mpoeq3dva NFinRRingxByBn0aNbNcoe1axCybn=0RiN,jNcoe1ixCyjn=iN,jN0R
45 7 30 mat0op NFinRRing0A=iN,jN0R
46 45 ad3antrrr NFinRRingxByBn0aNbNcoe1axCybn=0R0A=iN,jN0R
47 7 matring NFinRRingARing
48 8 ply1sca ARingA=ScalarQ
49 47 48 syl NFinRRingA=ScalarQ
50 49 ad3antrrr NFinRRingxByBn0aNbNcoe1axCybn=0RA=ScalarQ
51 50 fveq2d NFinRRingxByBn0aNbNcoe1axCybn=0R0A=0ScalarQ
52 44 46 51 3eqtr2d NFinRRingxByBn0aNbNcoe1axCybn=0RiN,jNcoe1ixCyjn=0ScalarQ
53 52 oveq1d NFinRRingxByBn0aNbNcoe1axCybn=0RiN,jNcoe1ixCyjn˙n×˙X=0ScalarQ˙n×˙X
54 8 ply1lmod ARingQLMod
55 47 54 syl NFinRRingQLMod
56 55 adantr NFinRRingxByBQLMod
57 47 adantr NFinRRingxByBARing
58 eqid mulGrpQ=mulGrpQ
59 8 6 58 5 9 ply1moncl ARingn0n×˙XL
60 57 59 sylan NFinRRingxByBn0n×˙XL
61 eqid ScalarQ=ScalarQ
62 eqid 0ScalarQ=0ScalarQ
63 eqid 0Q=0Q
64 9 61 4 62 63 lmod0vs QLModn×˙XL0ScalarQ˙n×˙X=0Q
65 56 60 64 syl2an2r NFinRRingxByBn00ScalarQ˙n×˙X=0Q
66 65 adantr NFinRRingxByBn0aNbNcoe1axCybn=0R0ScalarQ˙n×˙X=0Q
67 53 66 eqtrd NFinRRingxByBn0aNbNcoe1axCybn=0RiN,jNcoe1ixCyjn˙n×˙X=0Q
68 67 ex NFinRRingxByBn0aNbNcoe1axCybn=0RiN,jNcoe1ixCyjn˙n×˙X=0Q
69 68 imim2d NFinRRingxByBn0s<naNbNcoe1axCybn=0Rs<niN,jNcoe1ixCyjn˙n×˙X=0Q
70 69 ralimdva NFinRRingxByBn0s<naNbNcoe1axCybn=0Rn0s<niN,jNcoe1ixCyjn˙n×˙X=0Q
71 70 reximdv NFinRRingxByBs0n0s<naNbNcoe1axCybn=0Rs0n0s<niN,jNcoe1ixCyjn˙n×˙X=0Q
72 32 71 mpd NFinRRingxByBs0n0s<niN,jNcoe1ixCyjn˙n×˙X=0Q
73 2 3 decpmatval xCyBn0xCydecompPMatn=iN,jNcoe1ixCyjn
74 29 73 sylan NFinRRingxByBn0xCydecompPMatn=iN,jNcoe1ixCyjn
75 74 oveq1d NFinRRingxByBn0xCydecompPMatn˙n×˙X=iN,jNcoe1ixCyjn˙n×˙X
76 75 eqeq1d NFinRRingxByBn0xCydecompPMatn˙n×˙X=0QiN,jNcoe1ixCyjn˙n×˙X=0Q
77 76 imbi2d NFinRRingxByBn0s<nxCydecompPMatn˙n×˙X=0Qs<niN,jNcoe1ixCyjn˙n×˙X=0Q
78 77 ralbidva NFinRRingxByBn0s<nxCydecompPMatn˙n×˙X=0Qn0s<niN,jNcoe1ixCyjn˙n×˙X=0Q
79 78 rexbidv NFinRRingxByBs0n0s<nxCydecompPMatn˙n×˙X=0Qs0n0s<niN,jNcoe1ixCyjn˙n×˙X=0Q
80 72 79 mpbird NFinRRingxByBs0n0s<nxCydecompPMatn˙n×˙X=0Q
81 1 2 3 7 decpmatmul RRingxByBn0xCydecompPMatn=Ak=0nxdecompPMatkAydecompPMatnk
82 81 ad4ant234 NFinRRingxByBn0xCydecompPMatn=Ak=0nxdecompPMatkAydecompPMatnk
83 82 eqcomd NFinRRingxByBn0Ak=0nxdecompPMatkAydecompPMatnk=xCydecompPMatn
84 83 oveq1d NFinRRingxByBn0Ak=0nxdecompPMatkAydecompPMatnk˙n×˙X=xCydecompPMatn˙n×˙X
85 84 eqeq1d NFinRRingxByBn0Ak=0nxdecompPMatkAydecompPMatnk˙n×˙X=0QxCydecompPMatn˙n×˙X=0Q
86 85 imbi2d NFinRRingxByBn0s<nAk=0nxdecompPMatkAydecompPMatnk˙n×˙X=0Qs<nxCydecompPMatn˙n×˙X=0Q
87 86 ralbidva NFinRRingxByBn0s<nAk=0nxdecompPMatkAydecompPMatnk˙n×˙X=0Qn0s<nxCydecompPMatn˙n×˙X=0Q
88 87 rexbidv NFinRRingxByBs0n0s<nAk=0nxdecompPMatkAydecompPMatnk˙n×˙X=0Qs0n0s<nxCydecompPMatn˙n×˙X=0Q
89 80 88 mpbird NFinRRingxByBs0n0s<nAk=0nxdecompPMatkAydecompPMatnk˙n×˙X=0Q
90 11 12 20 89 mptnn0fsuppd NFinRRingxByBfinSupp0Ql0Ak=0lxdecompPMatkAydecompPMatlk˙l×˙X