This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. ) )