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 = ( Poly1 ` A )
mply1topmat.l 
|- L = ( Base ` Q )
mply1topmat.p 
|- P = ( Poly1 ` R )
mply1topmat.m 
|- .x. = ( .s ` P )
mply1topmat.e 
|- E = ( .g ` ( mulGrp ` P ) )
mply1topmat.y 
|- Y = ( var1 ` R )
Assertion mply1topmatcllem 
|- ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( ( I ( ( coe1 ` O ) ` k ) J ) .x. ( k E Y ) ) ) finSupp ( 0g ` P ) )

Proof

Step Hyp Ref Expression
1 mply1topmat.a 
 |-  A = ( N Mat R )
2 mply1topmat.q 
 |-  Q = ( Poly1 ` A )
3 mply1topmat.l 
 |-  L = ( Base ` Q )
4 mply1topmat.p 
 |-  P = ( Poly1 ` R )
5 mply1topmat.m 
 |-  .x. = ( .s ` P )
6 mply1topmat.e 
 |-  E = ( .g ` ( mulGrp ` P ) )
7 mply1topmat.y 
 |-  Y = ( var1 ` R )
8 nn0ex 
 |-  NN0 e. _V
9 8 a1i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> NN0 e. _V )
10 4 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
11 10 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> P e. LMod )
12 11 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> P e. LMod )
13 simp12 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> R e. Ring )
14 4 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
15 13 14 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> R = ( Scalar ` P ) )
16 eqid 
 |-  ( Base ` P ) = ( Base ` P )
17 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> ( I ( ( coe1 ` O ) ` k ) J ) e. _V )
18 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
19 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
20 19 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
21 18 20 syl 
 |-  ( R e. Ring -> ( mulGrp ` P ) e. Mnd )
22 21 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> ( mulGrp ` P ) e. Mnd )
23 22 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( mulGrp ` P ) e. Mnd )
24 23 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
25 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> k e. NN0 )
26 7 4 16 vr1cl 
 |-  ( R e. Ring -> Y e. ( Base ` P ) )
27 26 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. Ring /\ O e. L ) -> Y e. ( Base ` P ) )
28 27 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> Y e. ( Base ` P ) )
29 28 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> Y e. ( Base ` P ) )
30 19 16 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
31 30 6 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ k e. NN0 /\ Y e. ( Base ` P ) ) -> ( k E Y ) e. ( Base ` P ) )
32 24 25 29 31 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) /\ k e. NN0 ) -> ( k E Y ) e. ( Base ` P ) )
33 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
34 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
35 1 2 3 mptcoe1matfsupp 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( I ( ( coe1 ` O ) ` k ) J ) ) finSupp ( 0g ` R ) )
36 9 12 15 16 17 32 33 34 5 35 mptscmfsupp0 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ O e. L ) /\ I e. N /\ J e. N ) -> ( k e. NN0 |-> ( ( I ( ( coe1 ` O ) ` k ) J ) .x. ( k E Y ) ) ) finSupp ( 0g ` P ) )