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 = Poly 1 R
pmatcollpwscmat.c C = N Mat P
pmatcollpwscmat.b B = Base C
pmatcollpwscmat.m1 ˙ = C
pmatcollpwscmat.e1 × ˙ = mulGrp P
pmatcollpwscmat.x X = var 1 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 ˙ = 1 C
pmatcollpwscmat.m2 M = Q ˙ 1 ˙
Assertion pmatcollpwscmatlem1 N Fin R Ring L 0 Q E a N b N coe 1 a M b L P 0 mulGrp P var 1 R = if a = b U coe 1 Q L 0 P

Proof

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