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	|- P = ( Poly1 ` R )
	pmat0opsc.c	|- C = ( N Mat P )
	pmat0opsc.a	|- A = ( algSc ` P )
	pmat0opsc.z	|- .0. = ( 0g ` R )
Assertion	pmat0opsc	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( A ` .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmat0opsc.p	|- P = ( Poly1 ` R )
2		pmat0opsc.c	|- C = ( N Mat P )
3		pmat0opsc.a	|- A = ( algSc ` P )
4		pmat0opsc.z	|- .0. = ( 0g ` R )
5		eqid	|- ( 0g ` P ) = ( 0g ` P )
6	1 2 5	pmat0op	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( 0g ` P ) ) )
7	1 3 4 5	ply1scl0	|- ( R e. Ring -> ( A ` .0. ) = ( 0g ` P ) )
8	7	eqcomd	|- ( R e. Ring -> ( 0g ` P ) = ( A ` .0. ) )
9	8	adantl	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` P ) = ( A ` .0. ) )
10	9	mpoeq3dv	|- ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` P ) ) = ( i e. N , j e. N |-> ( A ` .0. ) ) )
11	6 10	eqtrd	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) = ( i e. N , j e. N |-> ( A ` .0. ) ) )