Metamath Proof Explorer


Theorem mply1topmatcllem

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

Ref Expression
Hypotheses mply1topmat.a A = N Mat R
mply1topmat.q Q = Poly 1 A
mply1topmat.l L = Base Q
mply1topmat.p P = Poly 1 R
mply1topmat.m · ˙ = P
mply1topmat.e E = mulGrp P
mply1topmat.y Y = var 1 R
Assertion mply1topmatcllem N Fin R Ring O L I N J N finSupp 0 P k 0 I coe 1 O k J · ˙ k E Y

Proof

Step Hyp Ref Expression
1 mply1topmat.a A = N Mat R
2 mply1topmat.q Q = Poly 1 A
3 mply1topmat.l L = Base Q
4 mply1topmat.p P = Poly 1 R
5 mply1topmat.m · ˙ = P
6 mply1topmat.e E = mulGrp P
7 mply1topmat.y Y = var 1 R
8 nn0ex 0 V
9 8 a1i N Fin R Ring O L I N J N 0 V
10 4 ply1lmod R Ring P LMod
11 10 3ad2ant2 N Fin R Ring O L P LMod
12 11 3ad2ant1 N Fin R Ring O L I N J N P LMod
13 simp12 N Fin R Ring O L I N J N R Ring
14 4 ply1sca R Ring R = Scalar P
15 13 14 syl N Fin R Ring O L I N J N R = Scalar P
16 eqid Base P = Base P
17 ovexd N Fin R Ring O L I N J N k 0 I coe 1 O k J V
18 eqid mulGrp P = mulGrp P
19 18 16 mgpbas Base P = Base mulGrp P
20 4 ply1ring R Ring P Ring
21 18 ringmgp P Ring mulGrp P Mnd
22 20 21 syl R Ring mulGrp P Mnd
23 22 3ad2ant2 N Fin R Ring O L mulGrp P Mnd
24 23 3ad2ant1 N Fin R Ring O L I N J N mulGrp P Mnd
25 24 adantr N Fin R Ring O L I N J N k 0 mulGrp P Mnd
26 simpr N Fin R Ring O L I N J N k 0 k 0
27 7 4 16 vr1cl R Ring Y Base P
28 27 3ad2ant2 N Fin R Ring O L Y Base P
29 28 3ad2ant1 N Fin R Ring O L I N J N Y Base P
30 29 adantr N Fin R Ring O L I N J N k 0 Y Base P
31 19 6 25 26 30 mulgnn0cld N Fin R Ring O L I N J N k 0 k E Y Base P
32 eqid 0 P = 0 P
33 eqid 0 R = 0 R
34 1 2 3 mptcoe1matfsupp N Fin R Ring O L I N J N finSupp 0 R k 0 I coe 1 O k J
35 9 12 15 16 17 31 32 33 5 34 mptscmfsupp0 N Fin R Ring O L I N J N finSupp 0 P k 0 I coe 1 O k J · ˙ k E Y