Theorem mat1comp

Description: The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	mamumat1cl.b	$$⊢B={\mathrm{Base}}_R$$
	mamumat1cl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mamumat1cl.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mamumat1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mamumat1cl.i	$$⊢I=\left(i\in M,j\in M⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
	mamumat1cl.m	$$⊢\phi \to M\in \mathrm{Fin}$$
Assertion	mat1comp	$$⊢\left(A\in M\wedge J\in M\right)\to AIJ=if\left(A=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mamumat1cl.b	$$⊢B={\mathrm{Base}}_R$$
2		mamumat1cl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
3		mamumat1cl.o	$$⊢\underset{\dot{}}{1}=1_R$$
4		mamumat1cl.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		mamumat1cl.i	$$⊢I=\left(i\in M,j\in M⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
6		mamumat1cl.m	$$⊢\phi \to M\in \mathrm{Fin}$$
7		eqeq1	$$⊢i=A\to \left(i=j\leftrightarrow A=j\right)$$
8	7	ifbid	$$⊢i=A\to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(A=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
9		eqeq2	$$⊢j=J\to \left(A=j\leftrightarrow A=J\right)$$
10	9	ifbid	$$⊢j=J\to if\left(A=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(A=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
11	3	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
12	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
13	11 12	ifex	$$⊢if\left(A=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
14	8 10 5 13	ovmpo	$$⊢\left(A\in M\wedge J\in M\right)\to AIJ=if\left(A=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$