Theorem pmat1opsc

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

	Ref	Expression
Hypotheses	pmat0opsc.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmat0opsc.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmat0opsc.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	pmat0opsc.z	⊢ 0 = ( 0g ‘ 𝑅 )
	pmat1opsc.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	pmat1opsc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmat0opsc.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmat0opsc.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmat0opsc.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
4		pmat0opsc.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		pmat1opsc.o	⊢ 1 = ( 1r ‘ 𝑅 )
6		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
7		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
8	1 2 6 7	pmat1op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) ) )
9	1 3 5 7	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
10	9	eqcomd	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑃 ) = ( 𝐴 ‘ 1 ) )
11	1 3 4 6	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
12	11	eqcomd	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑃 ) = ( 𝐴 ‘ 0 ) )
13	10 12	ifeq12d	⊢ ( 𝑅 ∈ Ring → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = if ( 𝑖 = 𝑗 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) )
14	13	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) = if ( 𝑖 = 𝑗 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) )
15	14	mpoeq3dv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r ‘ 𝑃 ) , ( 0g ‘ 𝑃 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) ) )
16	8 15	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , ( 𝐴 ‘ 1 ) , ( 𝐴 ‘ 0 ) ) ) )