Metamath Proof Explorer

Theorem matmulcell

Description: Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses matmulcell.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matmulcell.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matmulcell.m
Assertion matmulcell

Proof

Step Hyp Ref Expression
1 matmulcell.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matmulcell.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 matmulcell.m
4 1 2 matrcl ${⊢}{X}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
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{V}\right)\to {R}\mathrm{maMul}⟨{N},{N},{N}⟩={\cdot }_{{A}}$
7 6 3 syl6reqr
8 7 a1d
9 4 8 syl
11 10 impcom
13 12 oveqd
14 13 oveqd
15 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
16 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
17 simp1 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {R}\in \mathrm{Ring}$
18 4 simpld ${⊢}{X}\in {B}\to {N}\in \mathrm{Fin}$
19 18 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {N}\in \mathrm{Fin}$
20 19 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {N}\in \mathrm{Fin}$
21 1 15 2 matbas2i ${⊢}{X}\in {B}\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
22 21 adantr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
23 22 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {X}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
24 1 15 2 matbas2i ${⊢}{Y}\in {B}\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
25 24 adantl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
26 25 3ad2ant2 ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {Y}\in \left({{\mathrm{Base}}_{{R}}}^{\left({N}×{N}\right)}\right)$
27 simp3l ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\in {N}$
28 simp3r ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {J}\in {N}$
29 5 15 16 17 20 20 20 23 26 27 28 mamufv ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\left({X}\left({R}\mathrm{maMul}⟨{N},{N},{N}⟩\right){Y}\right){J}=\underset{{j}\in {N}}{{\sum }_{{R}}}\left(\left({I}{X}{j}\right){\cdot }_{{R}}\left({j}{Y}{J}\right)\right)$
30 14 29 eqtrd