Theorem marrepfval

Description: First substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019) (Proof shortened by AV, 2-Mar-2024)

	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	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)$$

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	2	fvexi	$$⊢B\in \mathrm{V}$$
6		fvexd	$$⊢\left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_R\in \mathrm{V}$$
7		mpoexga	$$⊢\left(B\in \mathrm{V}\wedge {\mathrm{Base}}_R\in \mathrm{V}\right)\to \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)\in \mathrm{V}$$
8	5 6 7	sylancr	$$⊢\left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \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)\in \mathrm{V}$$
9		oveq12	$$⊢\left(n=N\wedge r=R\right)\to n\mathrm{Mat}r=N\mathrm{Mat}R$$
10	9	fveq2d	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
11	1	fveq2i	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
12	2 11	eqtri	$$⊢B={\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}$$
13	10 12	eqtr4di	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)}=B$$
14		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
15	14	adantl	$$⊢\left(n=N\wedge r=R\right)\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
16		simpl	$$⊢\left(n=N\wedge r=R\right)\to n=N$$
17		fveq2	$$⊢r=R\to 0_r=0_R$$
18	17 4	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
19	18	ifeq2d	$$⊢r=R\to if\left(j=l,s,0_r\right)=if\left(j=l,s,\underset{\dot{}}{0}\right)$$
20	19	ifeq1d	$$⊢r=R\to if\left(i=k,if\left(j=l,s,0_r\right),imj\right)=if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)$$
21	20	adantl	$$⊢\left(n=N\wedge r=R\right)\to if\left(i=k,if\left(j=l,s,0_r\right),imj\right)=if\left(i=k,if\left(j=l,s,\underset{\dot{}}{0}\right),imj\right)$$
22	16 16 21	mpoeq123dv	$$⊢\left(n=N\wedge r=R\right)\to \left(i\in n,j\in n⟼if\left(i=k,if\left(j=l,s,0_r\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)$$
23	16 16 22	mpoeq123dv	$$⊢\left(n=N\wedge r=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,0_r\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)$$
24	13 15 23	mpoeq123dv	$$⊢\left(n=N\wedge r=R\right)\to \left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},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,0_r\right),imj\right)\right)\right)\right)=\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)$$
25		df-marrep	$$⊢\mathrm{matRRep}=\left(n\in \mathrm{V},r\in \mathrm{V}⟼\left(m\in {\mathrm{Base}}_{\left(n\mathrm{Mat}r\right)},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,0_r\right),imj\right)\right)\right)\right)\right)$$
26	24 25	ovmpoga	$$⊢\left(N\in \mathrm{V}\wedge R\in \mathrm{V}\wedge \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)\in \mathrm{V}\right)\to N\mathrm{matRRep}R=\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)$$
27	8 26	mpd3an3	$$⊢\left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to N\mathrm{matRRep}R=\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)$$
28	25	mpondm0	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to N\mathrm{matRRep}R=\varnothing$$
29		matbas0pc	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(N\mathrm{Mat}R\right)}=\varnothing$$
30	12 29	syl5eq	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to B=\varnothing$$
31	30	orcd	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \left(B=\varnothing \vee {\mathrm{Base}}_R=\varnothing \right)$$
32		0mpo0	$$⊢\left(B=\varnothing \vee {\mathrm{Base}}_R=\varnothing \right)\to \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)=\varnothing$$
33	31 32	syl	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to \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)=\varnothing$$
34	28 33	eqtr4d	$$⊢\neg \left(N\in \mathrm{V}\wedge R\in \mathrm{V}\right)\to N\mathrm{matRRep}R=\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)$$
35	27 34	pm2.61i	$$⊢N\mathrm{matRRep}R=\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)$$
36	3 35	eqtri	$$⊢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)$$