Metamath Proof Explorer

Theorem matbas2d

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

Ref Expression
Hypotheses matbas2.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matbas2.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
matbas2i.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
matbas2d.n ${⊢}{\phi }\to {N}\in \mathrm{Fin}$
matbas2d.r ${⊢}{\phi }\to {R}\in {V}$
matbas2d.c ${⊢}\left({\phi }\wedge {x}\in {N}\wedge {y}\in {N}\right)\to {C}\in {K}$
Assertion matbas2d ${⊢}{\phi }\to \left({x}\in {N},{y}\in {N}⟼{C}\right)\in {B}$

Proof

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