# Metamath Proof Explorer

## Theorem minmar1eval

Description: An entry 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 minmar1eval

### 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 minmar1val
7 6 3expb
9 simp3l ${⊢}\left({M}\in {B}\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\to {I}\in {N}$
10 simpl3r ${⊢}\left(\left({M}\in {B}\wedge \left({K}\in {N}\wedge {L}\in {N}\right)\wedge \left({I}\in {N}\wedge {J}\in {N}\right)\right)\wedge {i}={I}\right)\to {J}\in {N}$
11 4 fvexi
12 5 fvexi
13 11 12 ifex
14 ovex ${⊢}{i}{M}{j}\in \mathrm{V}$
15 13 14 ifex
16 15 a1i
17 eqeq1 ${⊢}{i}={I}\to \left({i}={K}↔{I}={K}\right)$
18 17 adantr ${⊢}\left({i}={I}\wedge {j}={J}\right)\to \left({i}={K}↔{I}={K}\right)$
19 eqeq1 ${⊢}{j}={J}\to \left({j}={L}↔{J}={L}\right)$
20 19 adantl ${⊢}\left({i}={I}\wedge {j}={J}\right)\to \left({j}={L}↔{J}={L}\right)$
21 20 ifbid
22 oveq12 ${⊢}\left({i}={I}\wedge {j}={J}\right)\to {i}{M}{j}={I}{M}{J}$
23 18 21 22 ifbieq12d