# Metamath Proof Explorer

## Theorem matassa

Description: Existence of the matrix algebra, see also the statement in Lang p. 505: "Then Mat_n(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015)

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

### 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{CRing}\right)\to {{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
4 1 matsca2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}=\mathrm{Scalar}\left({A}\right)$
5 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {\cdot }_{{A}}={\cdot }_{{A}}$
7 eqid ${⊢}{R}\mathrm{maMul}⟨{N},{N},{N}⟩={R}\mathrm{maMul}⟨{N},{N},{N}⟩$
8 1 7 matmulr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
9 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
10 1 matlmod ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{LMod}$
11 9 10 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{LMod}$
12 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
13 9 12 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{Ring}$
14 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{CRing}$
15 9 ad2antlr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}$
16 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}$
17 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
18 simpr1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}}_{{R}}$
19 simpr2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)$
20 simpr3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)$
21 2 15 7 16 16 16 17 18 19 20 mamuvs1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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(\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
22 3 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}}$
23 19 22 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}}$
24 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
25 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
26 eqid ${⊢}{N}×{N}={N}×{N}$
27 1 24 2 25 17 26 matvsca2 ${⊢}\left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\in {\mathrm{Base}}_{{A}}\right)\to {x}{\cdot }_{{A}}{y}=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{y}$
28 18 23 27 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}{\cdot }_{{A}}{y}=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{y}$
29 28 oveq1d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}{\cdot }_{{A}}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}=\left(\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}$
30 2 15 7 16 16 16 19 20 mamucl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)$
31 30 22 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}}$
32 1 24 2 25 17 26 matvsca2 ${⊢}\left({x}\in {\mathrm{Base}}_{{R}}\wedge {y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\in {\mathrm{Base}}_{{A}}\right)\to {x}{\cdot }_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
33 18 31 32 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}{\cdot }_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
34 21 29 33 3eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}{\cdot }_{{A}}{y}\right)\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}={x}{\cdot }_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
35 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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{CRing}$
36 35 2 17 7 16 16 16 19 18 20 mamuvs2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)\left(\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{z}\right)=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
37 20 22 eleqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}}$
38 1 24 2 25 17 26 matvsca2 ${⊢}\left({x}\in {\mathrm{Base}}_{{R}}\wedge {z}\in {\mathrm{Base}}_{{A}}\right)\to {x}{\cdot }_{{A}}{z}=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{z}$
39 18 37 38 syl2anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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}{\cdot }_{{A}}{z}=\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{z}$
40 39 oveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)\left({x}{\cdot }_{{A}}{z}\right)={y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right)\left(\left(\left({N}×{N}\right)×\left\{{x}\right\}\right){{\cdot }_{{R}}}_{f}{z}\right)$
41 36 40 33 3eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({x}\in {\mathrm{Base}}_{{R}}\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)\left({x}{\cdot }_{{A}}{z}\right)={x}{\cdot }_{{A}}\left({y}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){z}\right)$
42 3 4 5 6 8 11 13 14 34 41 isassad ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{AssAlg}$