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 Mat R$
	matecl.k	$⊢ K = {Base}_{R}$
Assertion	matecl	$⊢ (I \in N \land J \in N \land M \in {Base}_{A}) \to I M J \in K$

Proof

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

Metamath Proof Explorer

Theorem matecl

Proof