Theorem pmat0opsc

Description: The zero polynomial matrix over a ring represented as operation with "lifted scalars" (i.e. elements of the ring underlying the polynomial ring embedded into the polynomial ring by the scalar injection/algebraic scalars function algSc ). (Contributed by AV, 16-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		pmat0opsc.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmat0opsc.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmat0opsc.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
4		pmat0opsc.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
6	1 2 5	pmat0op	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) )
7	1 3 4 5	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
8	7	eqcomd	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑃 ) = ( 𝐴 ‘ 0 ) )
9	8	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝑃 ) = ( 𝐴 ‘ 0 ) )
10	9	mpoeq3dv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 0g ‘ 𝑃 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐴 ‘ 0 ) ) )
11	6 10	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐶 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝐴 ‘ 0 ) ) )