Theorem mat1ov

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

	Ref	Expression
Hypotheses	mat1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mat1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mat1ov.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mat1ov.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mat1ov.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	mat1ov.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	mat1ov.u	⊢ 𝑈 = ( 1r ‘ 𝐴 )
Assertion	mat1ov	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		mat1.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mat1.o	⊢ 1 = ( 1r ‘ 𝑅 )
3		mat1.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		mat1ov.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
5		mat1ov.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mat1ov.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
7		mat1ov.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
8		mat1ov.u	⊢ 𝑈 = ( 1r ‘ 𝐴 )
9	1 2 3	mat1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
10	4 5 9	syl2anc	⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
11	8 10	syl5eq	⊢ ( 𝜑 → 𝑈 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
12		eqeq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 = 𝑗 ↔ 𝐼 = 𝐽 ) )
13	12	ifbid	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )
15	2	fvexi	⊢ 1 ∈ V
16	3	fvexi	⊢ 0 ∈ V
17	15 16	ifex	⊢ if ( 𝐼 = 𝐽 , 1 , 0 ) ∈ V
18	17	a1i	⊢ ( 𝜑 → if ( 𝐼 = 𝐽 , 1 , 0 ) ∈ V )
19	11 14 6 7 18	ovmpod	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )