Theorem mat1ov

Description: Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018)

	Ref	Expression
Hypotheses	mat1.a	$$⊢A=N\mathrm{Mat}R$$
	mat1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mat1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mat1ov.n	$$⊢\phi \to N\in \mathrm{Fin}$$
	mat1ov.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	mat1ov.i	$$⊢\phi \to I\in N$$
	mat1ov.j	$$⊢\phi \to J\in N$$
	mat1ov.u	$$⊢U=1_A$$
Assertion	mat1ov	$$⊢\phi \to IUJ=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		mat1.a	$$⊢A=N\mathrm{Mat}R$$
2		mat1.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		mat1.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mat1ov.n	$$⊢\phi \to N\in \mathrm{Fin}$$
5		mat1ov.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		mat1ov.i	$$⊢\phi \to I\in N$$
7		mat1ov.j	$$⊢\phi \to J\in N$$
8		mat1ov.u	$$⊢U=1_A$$
9	1 2 3	mat1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 1_A=\left(i\in N,j\in N⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
10	4 5 9	syl2anc	$$⊢\phi \to 1_A=\left(i\in N,j\in N⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
11	8 10	eqtrid	$$⊢\phi \to U=\left(i\in N,j\in N⟼if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
12		eqeq12	$$⊢\left(i=I\wedge j=J\right)\to \left(i=j\leftrightarrow I=J\right)$$
13	12	ifbid	$$⊢\left(i=I\wedge j=J\right)\to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
14	13	adantl	$$⊢\left(\phi \wedge \left(i=I\wedge j=J\right)\right)\to if\left(i=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
15	2	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
16	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
17	15 16	ifex	$$⊢if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
19	11 14 6 7 18	ovmpod	$$⊢\phi \to IUJ=if\left(I=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$