matbas2d

Description: The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018)

Step	Hyp	Ref	Expression
1		matbas2.a	$⊢ A = N Mat R$
2		matbas2.k	$⊢ K = {Base}_{R}$
3		matbas2i.b	$⊢ B = {Base}_{A}$
4		matbas2d.n	$⊢ φ \to N \in Fin$
5		matbas2d.r	$⊢ φ \to R \in V$
6		matbas2d.c	$⊢ (φ \land x \in N \land y \in N) \to C \in K$
7	6	3expb	$⊢ (φ \land (x \in N \land y \in N)) \to C \in K$
8	7	ralrimivva	$⊢ φ \to \forall x \in N \forall y \in N C \in K$
9		eqid	$⊢ (x \in N, y \in N ⟼ C) = (x \in N, y \in N ⟼ C)$
10	9	fmpo	$⊢ \forall x \in N \forall y \in N C \in K \leftrightarrow (x \in N, y \in N ⟼ C) : N \times N ⟶ K$
11	8 10	sylib	$⊢ φ \to (x \in N, y \in N ⟼ C) : N \times N ⟶ K$
12	1 2	matbas2	$⊢ (N \in Fin \land R \in V) \to K^{(N \times N)} = {Base}_{A}$
13	4 5 12	syl2anc	$⊢ φ \to K^{(N \times N)} = {Base}_{A}$
14	3 13	eqtr4id	$⊢ φ \to B = K^{(N \times N)}$
15	14	eleq2d	$⊢ φ \to ((x \in N, y \in N ⟼ C) \in B \leftrightarrow (x \in N, y \in N ⟼ C) \in (K^{(N \times N)}))$
16	2	fvexi	$⊢ K \in V$
17	4 4	xpexd	$⊢ φ \to N \times N \in V$
18		elmapg	$⊢ (K \in V \land N \times N \in V) \to ((x \in N, y \in N ⟼ C) \in (K^{(N \times N)}) \leftrightarrow (x \in N, y \in N ⟼ C) : N \times N ⟶ K)$
19	16 17 18	sylancr	$⊢ φ \to ((x \in N, y \in N ⟼ C) \in (K^{(N \times N)}) \leftrightarrow (x \in N, y \in N ⟼ C) : N \times N ⟶ K)$
20	15 19	bitrd	$⊢ φ \to ((x \in N, y \in N ⟼ C) \in B \leftrightarrow (x \in N, y \in N ⟼ C) : N \times N ⟶ K)$
21	11 20	mpbird	$⊢ φ \to (x \in N, y \in N ⟼ C) \in B$

Metamath Proof Explorer