# Metamath Proof Explorer

## Theorem matecl

Description: Each entry (according to Wikipedia "Matrix (mathematics)", 30-Dec-2018, https://en.wikipedia.org/wiki/Matrix_(mathematics)#Definition (or element or component or coefficient or cell) of a matrix is an element of the underlying ring. (Contributed by AV, 16-Dec-2018)

Ref Expression
Hypotheses matecl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matecl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
Assertion matecl ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {I}{M}{J}\in {K}$

### Proof

Step Hyp Ref Expression
1 matecl.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matecl.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
4 1 3 matrcl ${⊢}{M}\in {\mathrm{Base}}_{{A}}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
5 4 3ad2ant3 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
6 1 2 matbas2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {{K}}^{\left({N}×{N}\right)}={\mathrm{Base}}_{{A}}$
7 6 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{{A}}={{K}}^{\left({N}×{N}\right)}$
8 7 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left({M}\in {\mathrm{Base}}_{{A}}↔{M}\in \left({{K}}^{\left({N}×{N}\right)}\right)\right)$
9 2 fvexi ${⊢}{K}\in \mathrm{V}$
10 9 a1i ${⊢}{R}\in \mathrm{V}\to {K}\in \mathrm{V}$
11 sqxpexg ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{V}$
12 elmapg ${⊢}\left({K}\in \mathrm{V}\wedge {N}×{N}\in \mathrm{V}\right)\to \left({M}\in \left({{K}}^{\left({N}×{N}\right)}\right)↔{M}:{N}×{N}⟶{K}\right)$
13 10 11 12 syl2anr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left({M}\in \left({{K}}^{\left({N}×{N}\right)}\right)↔{M}:{N}×{N}⟶{K}\right)$
14 ffnov ${⊢}{M}:{N}×{N}⟶{K}↔\left({M}Fn\left({N}×{N}\right)\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}\in {K}\right)$
15 oveq1 ${⊢}{i}={I}\to {i}{M}{j}={I}{M}{j}$
16 15 eleq1d ${⊢}{i}={I}\to \left({i}{M}{j}\in {K}↔{I}{M}{j}\in {K}\right)$
17 oveq2 ${⊢}{j}={J}\to {I}{M}{j}={I}{M}{J}$
18 17 eleq1d ${⊢}{j}={J}\to \left({I}{M}{j}\in {K}↔{I}{M}{J}\in {K}\right)$
19 16 18 rspc2v ${⊢}\left({I}\in {N}\wedge {J}\in {N}\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}\in {K}\to {I}{M}{J}\in {K}\right)$
20 19 com12 ${⊢}\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}\in {K}\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)$
21 20 adantl ${⊢}\left({M}Fn\left({N}×{N}\right)\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}\in {K}\right)\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)$
22 21 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left(\left({M}Fn\left({N}×{N}\right)\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{M}{j}\in {K}\right)\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)\right)$
23 14 22 syl5bi ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left({M}:{N}×{N}⟶{K}\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)\right)$
24 13 23 sylbid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left({M}\in \left({{K}}^{\left({N}×{N}\right)}\right)\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)\right)$
25 8 24 sylbid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to \left({M}\in {\mathrm{Base}}_{{A}}\to \left(\left({I}\in {N}\wedge {J}\in {N}\right)\to {I}{M}{J}\in {K}\right)\right)$
26 25 com13 ${⊢}\left({I}\in {N}\wedge {J}\in {N}\right)\to \left({M}\in {\mathrm{Base}}_{{A}}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {I}{M}{J}\in {K}\right)\right)$
27 26 ex ${⊢}{I}\in {N}\to \left({J}\in {N}\to \left({M}\in {\mathrm{Base}}_{{A}}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\to {I}{M}{J}\in {K}\right)\right)\right)$
28 27 3imp1 ${⊢}\left(\left({I}\in {N}\wedge {J}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\wedge \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)\right)\to {I}{M}{J}\in {K}$
29 5 28 mpdan ${⊢}\left({I}\in {N}\wedge {J}\in {N}\wedge {M}\in {\mathrm{Base}}_{{A}}\right)\to {I}{M}{J}\in {K}$