# Metamath Proof Explorer

## Theorem monmatcollpw

Description: The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid (but requires R to be commutative!). (Contributed by AV, 11-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses monmatcollpw.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
monmatcollpw.c ${⊢}{C}={N}\mathrm{Mat}{P}$
monmatcollpw.a ${⊢}{A}={N}\mathrm{Mat}{R}$
monmatcollpw.k ${⊢}{K}={\mathrm{Base}}_{{A}}$
monmatcollpw.0
monmatcollpw.e
monmatcollpw.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
monmatcollpw.m
monmatcollpw.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
Assertion monmatcollpw

### Proof

Step Hyp Ref Expression
1 monmatcollpw.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 monmatcollpw.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 monmatcollpw.a ${⊢}{A}={N}\mathrm{Mat}{R}$
4 monmatcollpw.k ${⊢}{K}={\mathrm{Base}}_{{A}}$
5 monmatcollpw.0
6 monmatcollpw.e
7 monmatcollpw.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
8 monmatcollpw.m
9 monmatcollpw.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
10 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {N}\in \mathrm{Fin}$
11 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
12 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
13 11 12 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Ring}$
14 13 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {P}\in \mathrm{Ring}$
15 11 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
16 simp2 ${⊢}\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\to {L}\in {ℕ}_{0}$
17 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
18 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
19 1 7 17 6 18 ply1moncl
20 15 16 19 syl2an
21 11 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
22 simp1 ${⊢}\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\to {M}\in {K}$
23 21 22 anim12i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {M}\in {K}\right)$
24 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {K}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {M}\in {K}\right)$
25 23 24 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {K}\right)$
26 9 3 4 1 2 mat2pmatbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {K}\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{C}}$
27 25 26 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {T}\left({M}\right)\in {\mathrm{Base}}_{{C}}$
28 20 27 jca
29 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
30 18 2 29 8 matvscl
31 10 14 28 30 syl21anc
32 simpr3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {I}\in {ℕ}_{0}$
33 2 29 decpmatval
34 31 32 33 syl2anc
35 14 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {P}\in \mathrm{Ring}$
37 3simpc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({i}\in {N}\wedge {j}\in {N}\right)$
38 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
39 2 29 18 8 38 matvscacell
40 35 36 37 39 syl3anc
41 40 fveq2d
42 41 fveq1d
43 22 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in {K}\right)$
44 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {K}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in {K}\right)$
45 43 44 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {K}\right)$
46 45 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {K}\right)$
47 eqid ${⊢}\mathrm{algSc}\left({P}\right)=\mathrm{algSc}\left({P}\right)$
48 9 3 4 1 47 mat2pmatvalel ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {K}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}{T}\left({M}\right){j}=\mathrm{algSc}\left({P}\right)\left({i}{M}{j}\right)$
49 46 37 48 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{T}\left({M}\right){j}=\mathrm{algSc}\left({P}\right)\left({i}{M}{j}\right)$
50 49 oveq2d
51 1 ply1assa ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{AssAlg}$
52 51 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {P}\in \mathrm{AssAlg}$
53 52 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {P}\in \mathrm{AssAlg}$
54 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
55 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
56 simp2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\in {N}$
57 simp3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {j}\in {N}$
58 4 eleq2i ${⊢}{M}\in {K}↔{M}\in {\mathrm{Base}}_{{A}}$
59 58 biimpi ${⊢}{M}\in {K}\to {M}\in {\mathrm{Base}}_{{A}}$
60 59 3ad2ant1 ${⊢}\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
61 60 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {M}\in {\mathrm{Base}}_{{A}}$
62 61 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {M}\in {\mathrm{Base}}_{{A}}$
63 3 54 55 56 57 62 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{M}{j}\in {\mathrm{Base}}_{{R}}$
64 1 ply1sca ${⊢}{R}\in \mathrm{CRing}\to {R}=\mathrm{Scalar}\left({P}\right)$
65 64 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}=\mathrm{Scalar}\left({P}\right)$
66 65 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \mathrm{Scalar}\left({P}\right)={R}$
67 66 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
68 67 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
69 68 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
70 63 69 eleqtrrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{M}{j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
72 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
73 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
74 eqid ${⊢}{\cdot }_{{P}}={\cdot }_{{P}}$
75 47 72 73 18 38 74 asclmul2
76 53 70 71 75 syl3anc
77 50 76 eqtrd
78 77 fveq2d
79 78 fveq1d
80 11 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {R}\in \mathrm{Ring}$
81 80 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
82 simp1r2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {L}\in {ℕ}_{0}$
83 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
84 83 54 1 7 74 17 6 coe1tm
85 81 63 82 84 syl3anc
86 85 fveq1d
87 42 79 86 3eqtrd
88 87 mpoeq3dva
89 21 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
90 89 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
91 3 83 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({z}\in {N},{w}\in {N}⟼{0}_{{R}}\right)$
92 90 91 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {0}_{{A}}=\left({z}\in {N},{w}\in {N}⟼{0}_{{R}}\right)$
93 5 92 syl5eq
94 eqidd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \left({z}={x}\wedge {w}={y}\right)\right)\to {0}_{{R}}={0}_{{R}}$
95 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {x}\in {N}$
96 simprr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {y}\in {N}$
97 fvexd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {0}_{{R}}\in \mathrm{V}$
98 93 94 95 96 97 ovmpod
99 98 eqcomd
100 99 ifeq2d
101 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)\right)=\left({i}\in {N},{j}\in {N}⟼\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)\right)$
102 oveq12 ${⊢}\left({i}={x}\wedge {j}={y}\right)\to {i}{M}{j}={x}{M}{y}$
103 102 ifeq1d ${⊢}\left({i}={x}\wedge {j}={y}\right)\to if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)=if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)$
104 103 mpteq2dv ${⊢}\left({i}={x}\wedge {j}={y}\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)\right)$
105 104 fveq1d ${⊢}\left({i}={x}\wedge {j}={y}\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)\right)\left({I}\right)$
106 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)\right)$
107 eqeq1 ${⊢}{l}={I}\to \left({l}={L}↔{I}={L}\right)$
108 107 ifbid ${⊢}{l}={I}\to if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)=if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)$
109 108 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge {l}={I}\right)\to if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)=if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)$
110 32 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {I}\in {ℕ}_{0}$
111 ovex ${⊢}{x}{M}{y}\in \mathrm{V}$
112 fvex ${⊢}{0}_{{R}}\in \mathrm{V}$
113 111 112 ifex ${⊢}if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)\in \mathrm{V}$
114 113 a1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)\in \mathrm{V}$
115 106 109 110 114 fvmptd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{x}{M}{y},{0}_{{R}}\right)\right)\left({I}\right)=if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)$
116 105 115 sylan9eqr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\wedge \left({i}={x}\wedge {j}={y}\right)\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)=if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)$
117 101 116 95 96 114 ovmpod ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge \left({x}\in {N}\wedge {y}\in {N}\right)\right)\to {x}\left({i}\in {N},{j}\in {N}⟼\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)\right){y}=if\left({I}={L},{x}{M}{y},{0}_{{R}}\right)$
118 ifov
119 118 a1i
120 100 117 119 3eqtr4d
121 120 ralrimivva
122 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {R}\in \mathrm{CRing}$
123 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)=\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)$
124 107 ifbid ${⊢}{l}={I}\to if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)=if\left({I}={L},{i}{M}{j},{0}_{{R}}\right)$
125 124 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {l}={I}\right)\to if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)=if\left({I}={L},{i}{M}{j},{0}_{{R}}\right)$
126 32 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {I}\in {ℕ}_{0}$
127 54 83 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
128 15 127 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
129 128 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
130 129 3ad2ant1 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
131 63 130 ifcld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to if\left({I}={L},{i}{M}{j},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
132 123 125 126 131 fvmptd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)=if\left({I}={L},{i}{M}{j},{0}_{{R}}\right)$
133 132 131 eqeltrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)\in {\mathrm{Base}}_{{R}}$
134 3 54 4 10 122 133 matbas2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to \left({i}\in {N},{j}\in {N}⟼\left({l}\in {ℕ}_{0}⟼if\left({l}={L},{i}{M}{j},{0}_{{R}}\right)\right)\left({I}\right)\right)\in {K}$
135 61 58 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {I}\in {ℕ}_{0}\right)\right)\to {M}\in {K}$
136 3 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
137 4 5 ring0cl
138 21 136 137 3syl