Theorem pmat1ovd

Description: Entries of the identity polynomial matrix over a ring, deduction form. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	pmatring.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatring.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmat0op.z	⊢ 0 = ( 0g ‘ 𝑃 )
	pmat1op.o	⊢ 1 = ( 1r ‘ 𝑃 )
	pmat1ovd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	pmat1ovd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	pmat1ovd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	pmat1ovd.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
	pmat1ovd.u	⊢ 𝑈 = ( 1r ‘ 𝐶 )
Assertion	pmat1ovd	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		pmatring.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmatring.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmat0op.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		pmat1op.o	⊢ 1 = ( 1r ‘ 𝑃 )
5		pmat1ovd.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
6		pmat1ovd.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		pmat1ovd.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
8		pmat1ovd.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
9		pmat1ovd.u	⊢ 𝑈 = ( 1r ‘ 𝐶 )
10	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11	6 10	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
12	2 4 3 5 11 7 8 9	mat1ov	⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )