Metamath Proof Explorer


Theorem dmatmat

Description: An N x N diagonal matrix over (the ring) R is an N x N matrix over (the ring) R . (Contributed by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatval.a
|- A = ( N Mat R )
dmatval.b
|- B = ( Base ` A )
dmatval.0
|- .0. = ( 0g ` R )
dmatval.d
|- D = ( N DMat R )
Assertion dmatmat
|- ( ( N e. Fin /\ R e. V ) -> ( M e. D -> M e. B ) )

Proof

Step Hyp Ref Expression
1 dmatval.a
 |-  A = ( N Mat R )
2 dmatval.b
 |-  B = ( Base ` A )
3 dmatval.0
 |-  .0. = ( 0g ` R )
4 dmatval.d
 |-  D = ( N DMat R )
5 1 2 3 4 dmatel
 |-  ( ( N e. Fin /\ R e. V ) -> ( M e. D <-> ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) ) )
6 simpl
 |-  ( ( M e. B /\ A. i e. N A. j e. N ( i =/= j -> ( i M j ) = .0. ) ) -> M e. B )
7 5 6 syl6bi
 |-  ( ( N e. Fin /\ R e. V ) -> ( M e. D -> M e. B ) )