Metamath Proof Explorer


Theorem mply1topmatcllem

Description: Lemma for mply1topmatcl . (Contributed by AV, 6-Oct-2019)

Ref Expression
Hypotheses mply1topmat.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
mply1topmat.q โŠข ๐‘„ = ( Poly1 โ€˜ ๐ด )
mply1topmat.l โŠข ๐ฟ = ( Base โ€˜ ๐‘„ )
mply1topmat.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
mply1topmat.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ƒ )
mply1topmat.e โŠข ๐ธ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
mply1topmat.y โŠข ๐‘Œ = ( var1 โ€˜ ๐‘… )
Assertion mply1topmatcllem ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ( ๐‘˜ โˆˆ โ„•0 โ†ฆ ( ( ๐ผ ( ( coe1 โ€˜ ๐‘‚ ) โ€˜ ๐‘˜ ) ๐ฝ ) ยท ( ๐‘˜ ๐ธ ๐‘Œ ) ) ) finSupp ( 0g โ€˜ ๐‘ƒ ) )

Proof

Step Hyp Ref Expression
1 mply1topmat.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 mply1topmat.q โŠข ๐‘„ = ( Poly1 โ€˜ ๐ด )
3 mply1topmat.l โŠข ๐ฟ = ( Base โ€˜ ๐‘„ )
4 mply1topmat.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
5 mply1topmat.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘ƒ )
6 mply1topmat.e โŠข ๐ธ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
7 mply1topmat.y โŠข ๐‘Œ = ( var1 โ€˜ ๐‘… )
8 nn0ex โŠข โ„•0 โˆˆ V
9 8 a1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ โ„•0 โˆˆ V )
10 4 ply1lmod โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘ƒ โˆˆ LMod )
11 10 3ad2ant2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โ†’ ๐‘ƒ โˆˆ LMod )
12 11 3ad2ant1 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ๐‘ƒ โˆˆ LMod )
13 simp12 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ๐‘… โˆˆ Ring )
14 4 ply1sca โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘… = ( Scalar โ€˜ ๐‘ƒ ) )
15 13 14 syl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ๐‘… = ( Scalar โ€˜ ๐‘ƒ ) )
16 eqid โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ๐‘ƒ )
17 ovexd โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐ผ ( ( coe1 โ€˜ ๐‘‚ ) โ€˜ ๐‘˜ ) ๐ฝ ) โˆˆ V )
18 eqid โŠข ( mulGrp โ€˜ ๐‘ƒ ) = ( mulGrp โ€˜ ๐‘ƒ )
19 18 16 mgpbas โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
20 4 ply1ring โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘ƒ โˆˆ Ring )
21 18 ringmgp โŠข ( ๐‘ƒ โˆˆ Ring โ†’ ( mulGrp โ€˜ ๐‘ƒ ) โˆˆ Mnd )
22 20 21 syl โŠข ( ๐‘… โˆˆ Ring โ†’ ( mulGrp โ€˜ ๐‘ƒ ) โˆˆ Mnd )
23 22 3ad2ant2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โ†’ ( mulGrp โ€˜ ๐‘ƒ ) โˆˆ Mnd )
24 23 3ad2ant1 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ( mulGrp โ€˜ ๐‘ƒ ) โˆˆ Mnd )
25 24 adantr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( mulGrp โ€˜ ๐‘ƒ ) โˆˆ Mnd )
26 simpr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ๐‘˜ โˆˆ โ„•0 )
27 7 4 16 vr1cl โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
28 27 3ad2ant2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
29 28 3ad2ant1 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
30 29 adantr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ๐‘Œ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
31 19 6 25 26 30 mulgnn0cld โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( ๐‘˜ ๐ธ ๐‘Œ ) โˆˆ ( Base โ€˜ ๐‘ƒ ) )
32 eqid โŠข ( 0g โ€˜ ๐‘ƒ ) = ( 0g โ€˜ ๐‘ƒ )
33 eqid โŠข ( 0g โ€˜ ๐‘… ) = ( 0g โ€˜ ๐‘… )
34 1 2 3 mptcoe1matfsupp โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ( ๐‘˜ โˆˆ โ„•0 โ†ฆ ( ๐ผ ( ( coe1 โ€˜ ๐‘‚ ) โ€˜ ๐‘˜ ) ๐ฝ ) ) finSupp ( 0g โ€˜ ๐‘… ) )
35 9 12 15 16 17 31 32 33 5 34 mptscmfsupp0 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘‚ โˆˆ ๐ฟ ) โˆง ๐ผ โˆˆ ๐‘ โˆง ๐ฝ โˆˆ ๐‘ ) โ†’ ( ๐‘˜ โˆˆ โ„•0 โ†ฆ ( ( ๐ผ ( ( coe1 โ€˜ ๐‘‚ ) โ€˜ ๐‘˜ ) ๐ฝ ) ยท ( ๐‘˜ ๐ธ ๐‘Œ ) ) ) finSupp ( 0g โ€˜ ๐‘ƒ ) )