Metamath Proof Explorer


Theorem cpmadumatpolylem2

Description: Lemma 2 for cpmadumatpoly . (Contributed by AV, 20-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses cpmadumatpoly.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
cpmadumatpoly.b โŠข ๐ต = ( Base โ€˜ ๐ด )
cpmadumatpoly.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
cpmadumatpoly.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
cpmadumatpoly.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
cpmadumatpoly.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
cpmadumatpoly.m0 โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
cpmadumatpoly.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
cpmadumatpoly.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
cpmadumatpoly.s โŠข ๐‘† = ( ๐‘ ConstPolyMat ๐‘… )
cpmadumatpoly.m1 โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
cpmadumatpoly.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
cpmadumatpoly.z โŠข ๐‘ = ( var1 โ€˜ ๐‘… )
cpmadumatpoly.d โŠข ๐ท = ( ( ๐‘ ยท 1 ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) )
cpmadumatpoly.j โŠข ๐ฝ = ( ๐‘ maAdju ๐‘ƒ )
cpmadumatpoly.w โŠข ๐‘Š = ( Base โ€˜ ๐‘Œ )
cpmadumatpoly.q โŠข ๐‘„ = ( Poly1 โ€˜ ๐ด )
cpmadumatpoly.x โŠข ๐‘‹ = ( var1 โ€˜ ๐ด )
cpmadumatpoly.m2 โŠข โˆ— = ( ยท๐‘  โ€˜ ๐‘„ )
cpmadumatpoly.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘„ ) )
cpmadumatpoly.u โŠข ๐‘ˆ = ( ๐‘ cPolyMatToMat ๐‘… )
Assertion cpmadumatpolylem2 ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ๐‘ˆ โˆ˜ ๐บ ) finSupp ( 0g โ€˜ ๐ด ) )

Proof

Step Hyp Ref Expression
1 cpmadumatpoly.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 cpmadumatpoly.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 cpmadumatpoly.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 cpmadumatpoly.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
5 cpmadumatpoly.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
6 cpmadumatpoly.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
7 cpmadumatpoly.m0 โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
8 cpmadumatpoly.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
9 cpmadumatpoly.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
10 cpmadumatpoly.s โŠข ๐‘† = ( ๐‘ ConstPolyMat ๐‘… )
11 cpmadumatpoly.m1 โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
12 cpmadumatpoly.1 โŠข 1 = ( 1r โ€˜ ๐‘Œ )
13 cpmadumatpoly.z โŠข ๐‘ = ( var1 โ€˜ ๐‘… )
14 cpmadumatpoly.d โŠข ๐ท = ( ( ๐‘ ยท 1 ) โˆ’ ( ๐‘‡ โ€˜ ๐‘€ ) )
15 cpmadumatpoly.j โŠข ๐ฝ = ( ๐‘ maAdju ๐‘ƒ )
16 cpmadumatpoly.w โŠข ๐‘Š = ( Base โ€˜ ๐‘Œ )
17 cpmadumatpoly.q โŠข ๐‘„ = ( Poly1 โ€˜ ๐ด )
18 cpmadumatpoly.x โŠข ๐‘‹ = ( var1 โ€˜ ๐ด )
19 cpmadumatpoly.m2 โŠข โˆ— = ( ยท๐‘  โ€˜ ๐‘„ )
20 cpmadumatpoly.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘„ ) )
21 cpmadumatpoly.u โŠข ๐‘ˆ = ( ๐‘ cPolyMatToMat ๐‘… )
22 fvexd โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( 0g โ€˜ ๐ด ) โˆˆ V )
23 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
24 23 anim2i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
25 24 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
26 25 ad2antrr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
27 10 3 4 0elcpmat โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ( 0g โ€˜ ๐‘Œ ) โˆˆ ๐‘† )
28 26 27 syl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( 0g โ€˜ ๐‘Œ ) โˆˆ ๐‘† )
29 1 2 3 4 6 7 8 5 9 10 chfacfisfcpmat โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐บ : โ„•0 โŸถ ๐‘† )
30 23 29 syl3anl2 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐บ : โ„•0 โŸถ ๐‘† )
31 30 anassrs โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐บ : โ„•0 โŸถ ๐‘† )
32 1 2 10 21 cpm2mf โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ๐‘ˆ : ๐‘† โŸถ ๐ต )
33 26 32 syl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐‘ˆ : ๐‘† โŸถ ๐ต )
34 ssidd โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐‘† โІ ๐‘† )
35 nn0ex โŠข โ„•0 โˆˆ V
36 35 a1i โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ โ„•0 โˆˆ V )
37 10 ovexi โŠข ๐‘† โˆˆ V
38 37 a1i โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐‘† โˆˆ V )
39 1 2 3 4 6 7 8 5 9 chfacffsupp โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐บ finSupp ( 0g โ€˜ ๐‘Œ ) )
40 39 anassrs โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐บ finSupp ( 0g โ€˜ ๐‘Œ ) )
41 eqid โŠข ( 0g โ€˜ ๐ด ) = ( 0g โ€˜ ๐ด )
42 eqid โŠข ( 0g โ€˜ ๐‘Œ ) = ( 0g โ€˜ ๐‘Œ )
43 1 21 3 4 41 42 m2cpminv0 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ( ๐‘ˆ โ€˜ ( 0g โ€˜ ๐‘Œ ) ) = ( 0g โ€˜ ๐ด ) )
44 23 43 sylan2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ˆ โ€˜ ( 0g โ€˜ ๐‘Œ ) ) = ( 0g โ€˜ ๐ด ) )
45 44 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ˆ โ€˜ ( 0g โ€˜ ๐‘Œ ) ) = ( 0g โ€˜ ๐ด ) )
46 45 ad2antrr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ๐‘ˆ โ€˜ ( 0g โ€˜ ๐‘Œ ) ) = ( 0g โ€˜ ๐ด ) )
47 22 28 31 33 34 36 38 40 46 fsuppcor โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ โ„• ) โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ( ๐‘ˆ โˆ˜ ๐บ ) finSupp ( 0g โ€˜ ๐ด ) )