Metamath Proof Explorer

Theorem pmatcollpwscmatlem1

Description: Lemma 1 for pmatcollpwscmat . (Contributed by AV, 2-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpwscmat.p 
|- P = ( Poly1 ` R )
pmatcollpwscmat.c 
|- C = ( N Mat P )
pmatcollpwscmat.b 
|- B = ( Base ` C )
pmatcollpwscmat.m1 
|- .* = ( .s ` C )
pmatcollpwscmat.e1 
|- .^ = ( .g ` ( mulGrp ` P ) )
pmatcollpwscmat.x 
|- X = ( var1 ` R )
pmatcollpwscmat.t 
|- T = ( N matToPolyMat R )
pmatcollpwscmat.a 
|- A = ( N Mat R )
pmatcollpwscmat.d 
|- D = ( Base ` A )
pmatcollpwscmat.u 
|- U = ( algSc ` P )
pmatcollpwscmat.k 
|- K = ( Base ` R )
pmatcollpwscmat.e2 
|- E = ( Base ` P )
pmatcollpwscmat.s 
|- S = ( algSc ` P )
pmatcollpwscmat.1 
|- .1. = ( 1r ` C )
pmatcollpwscmat.m2 
|- M = ( Q .* .1. )
Assertion pmatcollpwscmatlem1 
|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpwscmat.p 
 |-  P = ( Poly1 ` R )
2 pmatcollpwscmat.c 
 |-  C = ( N Mat P )
3 pmatcollpwscmat.b 
 |-  B = ( Base ` C )
4 pmatcollpwscmat.m1 
 |-  .* = ( .s ` C )
5 pmatcollpwscmat.e1 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
6 pmatcollpwscmat.x 
 |-  X = ( var1 ` R )
7 pmatcollpwscmat.t 
 |-  T = ( N matToPolyMat R )
8 pmatcollpwscmat.a 
 |-  A = ( N Mat R )
9 pmatcollpwscmat.d 
 |-  D = ( Base ` A )
10 pmatcollpwscmat.u 
 |-  U = ( algSc ` P )
11 pmatcollpwscmat.k 
 |-  K = ( Base ` R )
12 pmatcollpwscmat.e2 
 |-  E = ( Base ` P )
13 pmatcollpwscmat.s 
 |-  S = ( algSc ` P )
14 pmatcollpwscmat.1 
 |-  .1. = ( 1r ` C )
15 pmatcollpwscmat.m2 
 |-  M = ( Q .* .1. )
16 15 oveqi 
 |-  ( a M b ) = ( a ( Q .* .1. ) b )
17 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
18 17 anim2i 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( N e. Fin /\ P e. Ring ) )
19 simpr 
 |-  ( ( L e. NN0 /\ Q e. E ) -> Q e. E )
20 18 19 anim12i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( N e. Fin /\ P e. Ring ) /\ Q e. E ) )
21 df-3an 
 |-  ( ( N e. Fin /\ P e. Ring /\ Q e. E ) <-> ( ( N e. Fin /\ P e. Ring ) /\ Q e. E ) )
22 20 21 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( N e. Fin /\ P e. Ring /\ Q e. E ) )
23 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
24 2 12 23 14 4 scmatscmide 
 |-  ( ( ( N e. Fin /\ P e. Ring /\ Q e. E ) /\ ( a e. N /\ b e. N ) ) -> ( a ( Q .* .1. ) b ) = if ( a = b , Q , ( 0g ` P ) ) )
25 22 24 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( a ( Q .* .1. ) b ) = if ( a = b , Q , ( 0g ` P ) ) )
26 16 25 eqtrid 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( a M b ) = if ( a = b , Q , ( 0g ` P ) ) )
27 26 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( coe1 ` ( a M b ) ) = ( coe1 ` if ( a = b , Q , ( 0g ` P ) ) ) )
28 27 fveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( coe1 ` ( a M b ) ) ` L ) = ( ( coe1 ` if ( a = b , Q , ( 0g ` P ) ) ) ` L ) )
29 fvif 
 |-  ( coe1 ` if ( a = b , Q , ( 0g ` P ) ) ) = if ( a = b , ( coe1 ` Q ) , ( coe1 ` ( 0g ` P ) ) )
30 29 fveq1i 
 |-  ( ( coe1 ` if ( a = b , Q , ( 0g ` P ) ) ) ` L ) = ( if ( a = b , ( coe1 ` Q ) , ( coe1 ` ( 0g ` P ) ) ) ` L )
31 iffv 
 |-  ( if ( a = b , ( coe1 ` Q ) , ( coe1 ` ( 0g ` P ) ) ) ` L ) = if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) )
32 30 31 eqtri 
 |-  ( ( coe1 ` if ( a = b , Q , ( 0g ` P ) ) ) ` L ) = if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) )
33 28 32 eqtrdi 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( coe1 ` ( a M b ) ) ` L ) = if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) ) )
34 33 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
35 ovif 
 |-  ( if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( ( ( coe1 ` ( 0g ` P ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
36 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
37 1 23 36 coe1z 
 |-  ( R e. Ring -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
38 37 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( coe1 ` ( 0g ` P ) ) = ( NN0 X. { ( 0g ` R ) } ) )
39 38 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( coe1 ` ( 0g ` P ) ) ` L ) = ( ( NN0 X. { ( 0g ` R ) } ) ` L ) )
40 fvexd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` R ) e. _V )
41 simpl 
 |-  ( ( L e. NN0 /\ Q e. E ) -> L e. NN0 )
42 40 41 anim12i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( 0g ` R ) e. _V /\ L e. NN0 ) )
43 fvconst2g 
 |-  ( ( ( 0g ` R ) e. _V /\ L e. NN0 ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` L ) = ( 0g ` R ) )
44 42 43 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( NN0 X. { ( 0g ` R ) } ) ` L ) = ( 0g ` R ) )
45 39 44 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( coe1 ` ( 0g ` P ) ) ` L ) = ( 0g ` R ) )
46 45 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( coe1 ` ( 0g ` P ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` R ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
47 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
48 47 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> P e. LMod )
49 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
50 49 12 mgpbas 
 |-  E = ( Base ` ( mulGrp ` P ) )
51 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
52 49 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
53 17 52 syl 
 |-  ( R e. Ring -> ( mulGrp ` P ) e. Mnd )
54 0nn0 
 |-  0 e. NN0
55 54 a1i 
 |-  ( R e. Ring -> 0 e. NN0 )
56 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
57 56 1 12 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. E )
58 50 51 53 55 57 mulgnn0cld 
 |-  ( R e. Ring -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. E )
59 58 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. E )
60 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
61 eqid 
 |-  ( .s ` P ) = ( .s ` P )
62 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
63 12 60 61 62 23 lmod0vs 
 |-  ( ( P e. LMod /\ ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. E ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
64 48 59 63 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
65 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
66 65 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` P ) )
67 66 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
68 67 oveq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 0g ` R ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
69 68 eqeq1d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( 0g ` R ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) <-> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) ) )
70 69 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( 0g ` R ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) <-> ( ( 0g ` ( Scalar ` P ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) ) )
71 64 70 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( 0g ` R ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
72 46 71 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( coe1 ` ( 0g ` P ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( 0g ` P ) )
73 72 ifeq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( ( ( coe1 ` ( 0g ` P ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( 0g ` P ) ) )
74 73 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( ( ( coe1 ` ( 0g ` P ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( 0g ` P ) ) )
75 35 74 eqtrid 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( if ( a = b , ( ( coe1 ` Q ) ` L ) , ( ( coe1 ` ( 0g ` P ) ) ` L ) ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( 0g ` P ) ) )
76 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( L e. NN0 /\ Q e. E ) )
77 76 ancomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( Q e. E /\ L e. NN0 ) )
78 eqid 
 |-  ( coe1 ` Q ) = ( coe1 ` Q )
79 78 12 1 11 coe1fvalcl 
 |-  ( ( Q e. E /\ L e. NN0 ) -> ( ( coe1 ` Q ) ` L ) e. K )
80 77 79 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( coe1 ` Q ) ` L ) e. K )
81 65 eqcomd 
 |-  ( R e. Ring -> ( Scalar ` P ) = R )
82 81 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` P ) = R )
83 82 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
84 83 11 eqtr4di 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( Scalar ` P ) ) = K )
85 84 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( coe1 ` Q ) ` L ) e. ( Base ` ( Scalar ` P ) ) <-> ( ( coe1 ` Q ) ` L ) e. K ) )
86 85 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( coe1 ` Q ) ` L ) e. ( Base ` ( Scalar ` P ) ) <-> ( ( coe1 ` Q ) ` L ) e. K ) )
87 80 86 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( coe1 ` Q ) ` L ) e. ( Base ` ( Scalar ` P ) ) )
88 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
89 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
90 10 60 88 61 89 asclval 
 |-  ( ( ( coe1 ` Q ) ` L ) e. ( Base ` ( Scalar ` P ) ) -> ( U ` ( ( coe1 ` Q ) ` L ) ) = ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 1r ` P ) ) )
91 87 90 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( U ` ( ( coe1 ` Q ) ` L ) ) = ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 1r ` P ) ) )
92 1 56 49 51 ply1idvr1 
 |-  ( R e. Ring -> ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( 1r ` P ) )
93 92 eqcomd 
 |-  ( R e. Ring -> ( 1r ` P ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
94 93 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( 1r ` P ) = ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
95 94 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 1r ` P ) ) = ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
96 91 95 eqtr2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( U ` ( ( coe1 ` Q ) ` L ) ) )
97 96 ifeq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) -> if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( 0g ` P ) ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
98 97 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> if ( a = b , ( ( ( coe1 ` Q ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) , ( 0g ` P ) ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )
99 34 75 98 3eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( L e. NN0 /\ Q e. E ) ) /\ ( a e. N /\ b e. N ) ) -> ( ( ( coe1 ` ( a M b ) ) ` L ) ( .s ` P ) ( 0 ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = if ( a = b , ( U ` ( ( coe1 ` Q ) ` L ) ) , ( 0g ` P ) ) )