# Metamath Proof Explorer

## Theorem pmatcollpwscmatlem2

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

Ref Expression
Hypotheses pmatcollpwscmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pmatcollpwscmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pmatcollpwscmat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pmatcollpwscmat.m1
pmatcollpwscmat.e1
pmatcollpwscmat.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
pmatcollpwscmat.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
pmatcollpwscmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pmatcollpwscmat.d ${⊢}{D}={\mathrm{Base}}_{{A}}$
pmatcollpwscmat.u ${⊢}{U}=\mathrm{algSc}\left({P}\right)$
pmatcollpwscmat.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
pmatcollpwscmat.e2 ${⊢}{E}={\mathrm{Base}}_{{P}}$
pmatcollpwscmat.s ${⊢}{S}=\mathrm{algSc}\left({P}\right)$
pmatcollpwscmat.1
pmatcollpwscmat.m2
Assertion pmatcollpwscmatlem2

### Proof

Step Hyp Ref Expression
1 pmatcollpwscmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pmatcollpwscmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pmatcollpwscmat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pmatcollpwscmat.m1
5 pmatcollpwscmat.e1
6 pmatcollpwscmat.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
7 pmatcollpwscmat.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
8 pmatcollpwscmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
9 pmatcollpwscmat.d ${⊢}{D}={\mathrm{Base}}_{{A}}$
10 pmatcollpwscmat.u ${⊢}{U}=\mathrm{algSc}\left({P}\right)$
11 pmatcollpwscmat.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
12 pmatcollpwscmat.e2 ${⊢}{E}={\mathrm{Base}}_{{P}}$
13 pmatcollpwscmat.s ${⊢}{S}=\mathrm{algSc}\left({P}\right)$
14 pmatcollpwscmat.1
15 pmatcollpwscmat.m2
16 simpl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
17 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
18 17 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {R}\in \mathrm{Ring}$
19 simpr ${⊢}\left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\to {Q}\in {E}$
20 19 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Q}\in {E}\right)$
21 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {Q}\in {E}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {Q}\in {E}\right)$
22 20 21 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {Q}\in {E}\right)$
23 1 2 3 12 4 14 1pmatscmul
24 15 23 eqeltrid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {Q}\in {E}\right)\to {M}\in {B}$
25 22 24 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {M}\in {B}$
26 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {L}\in {ℕ}_{0}$
27 1 2 3 8 9 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {L}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{L}\in {D}$
28 18 25 26 27 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {M}\mathrm{decompPMat}{L}\in {D}$
29 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\mathrm{decompPMat}{L}\in {D}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {M}\mathrm{decompPMat}{L}\in {D}\right)$
30 16 28 29 sylanbrc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\mathrm{decompPMat}{L}\in {D}\right)$
31 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
32 7 8 9 1 31 mat2pmatval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\mathrm{decompPMat}{L}\in {D}\right)\to {T}\left({M}\mathrm{decompPMat}{L}\right)=\left({i}\in {N},{j}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({i}\left({M}\mathrm{decompPMat}{L}\right){j}\right)\right)$
33 30 32 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {T}\left({M}\mathrm{decompPMat}{L}\right)=\left({i}\in {N},{j}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({i}\left({M}\mathrm{decompPMat}{L}\right){j}\right)\right)$
34 18 25 26 3jca ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {L}\in {ℕ}_{0}\right)$
35 34 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {L}\in {ℕ}_{0}\right)$
36 3simpc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({i}\in {N}\wedge {j}\in {N}\right)$
37 1 2 3 decpmate ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {L}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\left({M}\mathrm{decompPMat}{L}\right){j}={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)$
38 35 36 37 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\left({M}\mathrm{decompPMat}{L}\right){j}={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)$
39 38 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \mathrm{algSc}\left({P}\right)\left({i}\left({M}\mathrm{decompPMat}{L}\right){j}\right)=\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\right)$
40 39 mpoeq3dva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({i}\left({M}\mathrm{decompPMat}{L}\right){j}\right)\right)=\left({i}\in {N},{j}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\right)\right)$
41 simp1lr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
42 simp2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\in {N}$
43 simp3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {j}\in {N}$
44 25 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {M}\in {B}$
45 2 12 3 42 43 44 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{M}{j}\in {E}$
46 26 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {L}\in {ℕ}_{0}$
47 eqid ${⊢}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)$
48 47 12 1 11 coe1fvalcl ${⊢}\left({i}{M}{j}\in {E}\wedge {L}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\in {K}$
49 45 46 48 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\in {K}$
50 eqid ${⊢}{\mathrm{var}}_{1}\left({R}\right)={\mathrm{var}}_{1}\left({R}\right)$
51 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
52 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
53 eqid ${⊢}{\cdot }_{{\mathrm{mulGrp}}_{{P}}}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
54 11 1 50 51 52 53 31 ply1scltm ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\in {K}\right)\to \mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)$
55 41 49 54 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)$
56 55 mpoeq3dva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\mathrm{algSc}\left({P}\right)\left({\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)$
57 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pmatcollpwscmatlem1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)=if\left({a}={b},{U}\left({\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\right),{0}_{{P}}\right)$
58 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)$
59 oveq12 ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {i}{M}{j}={a}{M}{b}$
60 59 fveq2d ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({a}{M}{b}\right)$
61 60 fveq1d ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)={\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right)$
62 61 oveq1d ${⊢}\left({i}={a}\wedge {j}={b}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)={\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)$
63 62 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\wedge \left({i}={a}\wedge {j}={b}\right)\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)={\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)$
64 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}\in {N}$
65 simprr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {b}\in {N}$
66 ovexd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\in \mathrm{V}$
67 58 63 64 65 66 ovmpod ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge \left({a}\in {N}\wedge {b}\in {N}\right)\right)\to {a}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right){b}={\mathrm{coe}}_{1}\left({a}{M}{b}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)$
68 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {N}\in \mathrm{Fin}$
69 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
70 69 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {P}\in \mathrm{Ring}$
71 70 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {P}\in \mathrm{Ring}$
72 pm3.22 ${⊢}\left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\to \left({Q}\in {E}\wedge {L}\in {ℕ}_{0}\right)$
73 72 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({Q}\in {E}\wedge {L}\in {ℕ}_{0}\right)$
74 eqid ${⊢}{\mathrm{coe}}_{1}\left({Q}\right)={\mathrm{coe}}_{1}\left({Q}\right)$
75 74 12 1 11 coe1fvalcl ${⊢}\left({Q}\in {E}\wedge {L}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\in {K}$
76 73 75 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\in {K}$
77 1 10 11 12 ply1sclcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\in {K}\right)\to {U}\left({\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\right)\in {E}$
78 18 76 77 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to {U}\left({\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\right)\in {E}$
79 68 71 78 3jca ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\wedge {U}\left({\mathrm{coe}}_{1}\left({Q}\right)\left({L}\right)\right)\in {E}\right)$
80 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
81 2 12 80 14 4 scmatscmide
82 79 81 sylan
83 57 67 82 3eqtr4d
84 83 ralrimivva
85 0nn0 ${⊢}0\in {ℕ}_{0}$
86 85 a1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to 0\in {ℕ}_{0}$
87 11 1 50 51 52 53 12 ply1tmcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right)\in {K}\wedge 0\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\in {E}$
88 41 49 86 87 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\in {E}$
89 2 12 3 68 71 88 matbas2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({L}\in {ℕ}_{0}\wedge {Q}\in {E}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({L}\right){\cdot }_{{P}}\left(0{\cdot }_{{\mathrm{mulGrp}}_{{P}}}{\mathrm{var}}_{1}\left({R}\right)\right)\right)\in {B}$
90 1 2 3 12 4 14 1pmatscmul
91 68 18 78 90 syl3anc
92 2 3 eqmat
93 89 91 92 syl2anc
94 84 93 mpbird
95 56 94 eqtrd
96 33 40 95 3eqtrd