# Metamath Proof Explorer

## Theorem minmar1fval

Description: First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

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

### Proof

Step Hyp Ref Expression
1 minmar1fval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 minmar1fval.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 minmar1fval.q ${⊢}{Q}={N}\mathrm{minMatR1}{R}$
4 minmar1fval.o
5 minmar1fval.z
6 oveq12 ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{r}={N}\mathrm{Mat}{R}$
7 6 1 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}\mathrm{Mat}{r}={A}$
8 7 fveq2d ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}={\mathrm{Base}}_{{A}}$
9 8 2 syl6eqr ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}={B}$
10 simpl ${⊢}\left({n}={N}\wedge {r}={R}\right)\to {n}={N}$
11 fveq2 ${⊢}{r}={R}\to {1}_{{r}}={1}_{{R}}$
12 11 4 syl6eqr
13 fveq2 ${⊢}{r}={R}\to {0}_{{r}}={0}_{{R}}$
14 13 5 syl6eqr
15 12 14 ifeq12d
16 15 ifeq1d
18 10 10 17 mpoeq123dv
19 10 10 18 mpoeq123dv
20 9 19 mpteq12dv
21 df-minmar1 ${⊢}\mathrm{minMatR1}=\left({n}\in \mathrm{V},{r}\in \mathrm{V}⟼\left({m}\in {\mathrm{Base}}_{\left({n}\mathrm{Mat}{r}\right)}⟼\left({k}\in {n},{l}\in {n}⟼\left({i}\in {n},{j}\in {n}⟼if\left({i}={k},if\left({j}={l},{1}_{{r}},{0}_{{r}}\right),{i}{m}{j}\right)\right)\right)\right)\right)$
22 2 fvexi ${⊢}{B}\in \mathrm{V}$
23 22 mptex
24 20 21 23 ovmpoa
25 21 mpondm0 ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {N}\mathrm{minMatR1}{R}=\varnothing$
26 mpt0
27 25 26 syl6eqr
28 1 fveq2i ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}$
29 2 28 eqtri ${⊢}{B}={\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}$
30 matbas0pc ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left({N}\mathrm{Mat}{R}\right)}=\varnothing$
31 29 30 syl5eq ${⊢}¬\left({N}\in \mathrm{V}\wedge {R}\in \mathrm{V}\right)\to {B}=\varnothing$
32 31 mpteq1d
33 27 32 eqtr4d
34 24 33 pm2.61i
35 3 34 eqtri