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