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	$$⊢\underset{\dot{}}{1}=1_R$$
	minmar1fval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	minmar1eval	$$⊢\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\left(KQ\left(M\right)L\right)J=if\left(I=K,if\left(J=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),IMJ\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	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)$$
7	6	3expb	$$⊢\left(M\in B\wedge \left(K\in N\wedge L\in N\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)$$
8	7	3adant3	$$⊢\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 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)$$
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	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
12	5	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
13	11 12	ifex	$$⊢if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
14		ovex	$$⊢iMj\in \mathrm{V}$$
15	13 14	ifex	$$⊢if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\in \mathrm{V}$$
16	15	a1i	$$⊢\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 \left(i=I\wedge j=J\right)\right)\to if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\in \mathrm{V}$$
17		eqeq1	$$⊢i=I\to \left(i=K\leftrightarrow I=K\right)$$
18	17	adantr	$$⊢\left(i=I\wedge j=J\right)\to \left(i=K\leftrightarrow I=K\right)$$
19		eqeq1	$$⊢j=J\to \left(j=L\leftrightarrow J=L\right)$$
20	19	adantl	$$⊢\left(i=I\wedge j=J\right)\to \left(j=L\leftrightarrow J=L\right)$$
21	20	ifbid	$$⊢\left(i=I\wedge j=J\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		oveq12	$$⊢\left(i=I\wedge j=J\right)\to iMj=IMJ$$
23	18 21 22	ifbieq12d	$$⊢\left(i=I\wedge j=J\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)$$
24	23	adantl	$$⊢\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 \left(i=I\wedge j=J\right)\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)$$
25	9 10 16 24	ovmpodv2	$$⊢\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 \left(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)\to I\left(KQ\left(M\right)L\right)J=if\left(I=K,if\left(J=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),IMJ\right)\right)$$
26	8 25	mpd	$$⊢\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\left(KQ\left(M\right)L\right)J=if\left(I=K,if\left(J=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),IMJ\right)$$