# Metamath Proof Explorer

## Theorem minmar1val

Description: Third 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 minmar1val

### 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 1 2 3 4 5 minmar1val0
8 simp2 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\wedge {L}\in {N}\right)\to {K}\in {N}$
9 simpl3 ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\wedge {L}\in {N}\right)\wedge {k}={K}\right)\to {L}\in {N}$
10 1 2 matrcl ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{V}\right)$
11 10 simpld ${⊢}{M}\in {B}\to {N}\in \mathrm{Fin}$
12 11 11 jca ${⊢}{M}\in {B}\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
13 12 3ad2ant1 ${⊢}\left({M}\in {B}\wedge {K}\in {N}\wedge {L}\in {N}\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
14 13 adantr ${⊢}\left(\left({M}\in {B}\wedge {K}\in {N}\wedge {L}\in {N}\right)\wedge \left({k}={K}\wedge {l}={L}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)$
15 mpoexga
16 14 15 syl
17 eqeq2 ${⊢}{k}={K}\to \left({i}={k}↔{i}={K}\right)$
18 17 adantr ${⊢}\left({k}={K}\wedge {l}={L}\right)\to \left({i}={k}↔{i}={K}\right)$
19 eqeq2 ${⊢}{l}={L}\to \left({j}={l}↔{j}={L}\right)$
20 19 ifbid