Theorem pmat1op

Description: The identity polynomial matrix over a ring represented as operation. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	pmatring.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmatring.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmat0op.z	⊢ 0 = ( 0g ‘ 𝑃 )
	pmat1op.o	⊢ 1 = ( 1r ‘ 𝑃 )
Assertion	pmat1op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 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	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
6	2 4 3	mat1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
7	5 6	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )