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𝑃 ) )