# Metamath Proof Explorer

## Theorem marrepval0

Description: Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019)

Ref Expression
Hypotheses marrepfval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
marrepfval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
marrepfval.q ${⊢}{Q}={N}\mathrm{matRRep}{R}$
marrepfval.z
Assertion marrepval0

### Proof

Step Hyp Ref Expression
1 marrepfval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 marrepfval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 marrepfval.q ${⊢}{Q}={N}\mathrm{matRRep}{R}$
4 marrepfval.z
5 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
6 5 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
7 6 6 jca ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
8 7 adantr ${⊢}\left({M}\in {B}\wedge {S}\in {\mathrm{Base}}_{{R}}\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
9 mpoexga
10 8 9 syl
11 ifeq1
13 oveq ${⊢}{m}={M}\to {i}{m}{j}={i}{M}{j}$
14 13 adantr ${⊢}\left({m}={M}\wedge {s}={S}\right)\to {i}{m}{j}={i}{M}{j}$