Theorem marrepval0

Description: Second substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019)

	Ref	Expression
Hypotheses	marrepfval.a	$$⊢A=N\mathrm{Mat}R$$
	marrepfval.b	$$⊢B={\mathrm{Base}}_A$$
	marrepfval.q	$$⊢Q=N\mathrm{matRRep}R$$
	marrepfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	marrepval0	$$⊢\left(M\in B\wedge S\in {\mathrm{Base}}_R\right)\to MQS=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		marrepfval.a	$$⊢A=N\mathrm{Mat}R$$
2		marrepfval.b	$$⊢B={\mathrm{Base}}_A$$
3		marrepfval.q	$$⊢Q=N\mathrm{matRRep}R$$
4		marrepfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5	1 2	matrcl	$$⊢M\in B\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{V}\right)$$
6	5	simpld	$$⊢M\in B\to N\in \mathrm{Fin}$$
7	6 6	jca	$$⊢M\in B\to \left(N\in \mathrm{Fin}\wedge N\in \mathrm{Fin}\right)$$
8	7	adantr	$$⊢\left(M\in B\wedge S\in {\mathrm{Base}}_R\right)\to \left(N\in \mathrm{Fin}\wedge N\in \mathrm{Fin}\right)$$
9		mpoexga	$$⊢\left(N\in \mathrm{Fin}\wedge N\in \mathrm{Fin}\right)\to \left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)\in \mathrm{V}$$
10	8 9	syl	$$⊢\left(M\in B\wedge S\in {\mathrm{Base}}_R\right)\to \left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)\in \mathrm{V}$$
11		ifeq1	$$⊢s=S\to if\left(j=l,s,\underset{\dot{}}{0}\right)=if\left(j=l,S,\underset{\dot{}}{0}\right)$$
12	11	adantl	$$⊢\left(m=M\wedge s=S\right)\to if\left(j=l,s,\underset{\dot{}}{0}\right)=if\left(j=l,S,\underset{\dot{}}{0}\right)$$
13		oveq	$$⊢m=M\to imj=iMj$$
14	13	adantr	$$⊢\left(m=M\wedge s=S\right)\to imj=iMj$$
15	12 14	ifeq12d	$$⊢\left(m=M\wedge s=S\right)\to if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)=if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)$$
16	15	mpoeq3dv	$$⊢\left(m=M\wedge s=S\right)\to \left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)\right)=\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)$$
17	16	mpoeq3dv	$$⊢\left(m=M\wedge s=S\right)\to \left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)\right)\right)=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$
18	1 2 3 4	marrepfval	$$⊢Q=\left(m\in B,s\in {\mathrm{Base}}_R⟼\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)\right)\right)\right)$$
19	17 18	ovmpoga	$$⊢\left(M\in B\wedge S\in {\mathrm{Base}}_R\wedge \left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)\in \mathrm{V}\right)\to MQS=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$
20	10 19	mpd3an3	$$⊢\left(M\in B\wedge S\in {\mathrm{Base}}_R\right)\to MQS=\left(k\in N,l\in N⟼\left(i\in N,j\in N⟼if\left(i=k,if\left(j=l,S,\underset{\dot{}}{0}\right),iMj\right)\right)\right)$$