Theorem mat0op

Description: Value of a zero matrix as operation. (Contributed by AV, 2-Dec-2018)

	Ref	Expression
Hypotheses	mat0op.a	|- A = ( N Mat R )
	mat0op.z	|- .0. = ( 0g ` R )
Assertion	mat0op	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> .0. ) )

Proof

Step	Hyp	Ref	Expression
1		mat0op.a	|- A = ( N Mat R )
2		mat0op.z	|- .0. = ( 0g ` R )
3		eqid	|- ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
4	1 3	mat0	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` ( R freeLMod ( N X. N ) ) ) = ( 0g ` A ) )
5		fconstmpo	|- ( ( N X. N ) X. { ( 0g ` R ) } ) = ( i e. N , j e. N |-> ( 0g ` R ) )
6		simpr	|- ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )
7		sqxpexg	|- ( N e. Fin -> ( N X. N ) e. _V )
8	7	adantr	|- ( ( N e. Fin /\ R e. Ring ) -> ( N X. N ) e. _V )
9		eqid	|- ( 0g ` R ) = ( 0g ` R )
10	3 9	frlm0	|- ( ( R e. Ring /\ ( N X. N ) e. _V ) -> ( ( N X. N ) X. { ( 0g ` R ) } ) = ( 0g ` ( R freeLMod ( N X. N ) ) ) )
11	6 8 10	syl2anc	|- ( ( N e. Fin /\ R e. Ring ) -> ( ( N X. N ) X. { ( 0g ` R ) } ) = ( 0g ` ( R freeLMod ( N X. N ) ) ) )
12	2	eqcomi	|- ( 0g ` R ) = .0.
13	12	a1i	|- ( ( i e. N /\ j e. N ) -> ( 0g ` R ) = .0. )
14	13	mpoeq3ia	|- ( i e. N , j e. N |-> ( 0g ` R ) ) = ( i e. N , j e. N |-> .0. )
15	14	a1i	|- ( ( N e. Fin /\ R e. Ring ) -> ( i e. N , j e. N |-> ( 0g ` R ) ) = ( i e. N , j e. N |-> .0. ) )
16	5 11 15	3eqtr3a	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` ( R freeLMod ( N X. N ) ) ) = ( i e. N , j e. N |-> .0. ) )
17	4 16	eqtr3d	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` A ) = ( i e. N , j e. N |-> .0. ) )