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	$$⊢\underset{\dot{}}{1}=1_R$$
	minmar1fval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	minmar1val	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to KQ\left(M\right)L=\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)$$

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	$$⊢\underset{\dot{}}{1}=1_R$$
5		minmar1fval.z	$$⊢\underset{\dot{}}{0}=0_R$$
6	1 2 3 4 5	minmar1val0	$$⊢M\in B\to Q\left(M\right)=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$
7	6	3ad2ant1	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to Q\left(M\right)=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$
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	$$⊢\left(N\in \mathrm{Fin}\wedge N\in \mathrm{Fin}\right)\to \left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in \mathrm{V}$$
16	14 15	syl	$$⊢\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(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\in \mathrm{V}$$
17		eqeq2	$$⊢k=K\to \left(i=k\leftrightarrow i=K\right)$$
18	17	adantr	$$⊢\left(k=K\wedge l=L\right)\to \left(i=k\leftrightarrow i=K\right)$$
19		eqeq2	$$⊢l=L\to \left(j=l\leftrightarrow j=L\right)$$
20	19	ifbid	$$⊢l=L\to if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
21	20	adantl	$$⊢\left(k=K\wedge l=L\right)\to if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
22	18 21	ifbieq1d	$$⊢\left(k=K\wedge l=L\right)\to if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)=if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)$$
23	22	mpoeq3dv	$$⊢\left(k=K\wedge l=L\right)\to \left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)=\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)$$
24	23	adantl	$$⊢\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(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)=\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)$$
25	8 9 16 24	ovmpodv2	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to \left(Q\left(M\right)=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\right)\to KQ\left(M\right)L=\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$
26	7 25	mpd	$$⊢\left(M\in B\wedge K\in N\wedge L\in N\right)\to KQ\left(M\right)L=\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)$$