# Metamath Proof Explorer

## Theorem matring

Description: Existence of the matrix ring, see also the statement in Lang p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis matassa.a ${⊢}{A}={N}\mathrm{Mat}{R}$
Assertion matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$

### Proof

Step Hyp Ref Expression
1 matassa.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 1 2 matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
4 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {+}_{{A}}={+}_{{A}}$
5 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
6 1 5 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
7 1 matgrp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Grp}$
8 simp1r ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {R}\in \mathrm{Ring}$
9 simp1l ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {N}\in \mathrm{Fin}$
10 simp2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
11 simp3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
12 2 8 5 9 9 9 10 11 mamucl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
13 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {R}\in \mathrm{Ring}$
14 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {N}\in \mathrm{Fin}$
15 simpr1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
16 simpr2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
17 simpr3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
18 2 13 14 14 14 14 15 16 17 5 5 5 5 mamuass ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}={x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
19 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
20 2 13 5 14 14 14 19 15 16 17 mamudir ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({y}{{+}_{{R}}}_{f}{z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){{+}_{{R}}}_{f}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
21 3 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
22 16 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{A}}$
23 17 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{{A}}$
24 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
25 eqid ${⊢}{+}_{{A}}={+}_{{A}}$
26 1 24 25 19 matplusg2 ${⊢}\left({y}\in {\mathrm{Base}}_{{A}}\wedge {z}\in {\mathrm{Base}}_{{A}}\right)\to {y}{+}_{{A}}{z}={y}{{+}_{{R}}}_{f}{z}$
27 22 23 26 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {y}{+}_{{A}}{z}={y}{{+}_{{R}}}_{f}{z}$
28 27 oveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({y}{+}_{{A}}{z}\right)={x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({y}{{+}_{{R}}}_{f}{z}\right)$
29 2 13 5 14 14 14 15 16 mamucl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
30 29 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\in {\mathrm{Base}}_{{A}}$
31 2 13 5 14 14 14 15 17 mamucl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
32 31 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}$
33 1 24 25 19 matplusg2 ${⊢}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\in {\mathrm{Base}}_{{A}}\wedge {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}\right)\to \left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){+}_{{A}}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){{+}_{{R}}}_{f}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
34 30 32 33 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){+}_{{A}}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){{+}_{{R}}}_{f}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
35 20 28 34 3eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({y}{+}_{{A}}{z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){y}\right){+}_{{A}}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
36 2 13 5 14 14 14 19 15 16 17 mamudi ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}{{+}_{{R}}}_{f}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){{+}_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
37 15 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{A}}$
38 1 24 25 19 matplusg2 ${⊢}\left({x}\in {\mathrm{Base}}_{{A}}\wedge {y}\in {\mathrm{Base}}_{{A}}\right)\to {x}{+}_{{A}}{y}={x}{{+}_{{R}}}_{f}{y}$
39 37 22 38 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {x}{+}_{{A}}{y}={x}{{+}_{{R}}}_{f}{y}$
40 39 oveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}{+}_{{A}}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}=\left({x}{{+}_{{R}}}_{f}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}$
41 2 13 5 14 14 14 16 17 mamucl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
42 41 21 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to {y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}$
43 1 24 25 19 matplusg2 ${⊢}\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}\wedge {y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}\right)\to \left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){+}_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){{+}_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
44 32 42 43 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){+}_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){{+}_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
45 36 40 44 3eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\wedge {z}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\right)\to \left({x}{+}_{{A}}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}=\left({x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right){+}_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
46 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
47 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
48 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
49 eqid ${⊢}\left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{1}_{{R}},{0}_{{R}}\right)\right)=\left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{1}_{{R}},{0}_{{R}}\right)\right)$
50 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\in \mathrm{Fin}$
51 2 46 47 48 49 50 mamumat1cl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
52 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {R}\in \mathrm{Ring}$
53 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {N}\in \mathrm{Fin}$
54 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
55 2 52 47 48 49 53 53 5 54 mamulid ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to \left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{1}_{{R}},{0}_{{R}}\right)\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){x}={x}$
56 2 52 47 48 49 53 53 5 54 mamurid ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)\right)\to {x}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left({a}\in {N},{b}\in {N}⟼if\left({a}={b},{1}_{{R}},{0}_{{R}}\right)\right)={x}$
57 3 4 6 7 12 18 35 45 51 55 56 isringd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$