Description: A scalar matrix can be expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019) (Revised by AV, 18-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | scmatval.k | |- K = ( Base ` R ) |
|
| scmatval.a | |- A = ( N Mat R ) |
||
| scmatval.b | |- B = ( Base ` A ) |
||
| scmatval.1 | |- .1. = ( 1r ` A ) |
||
| scmatval.t | |- .x. = ( .s ` A ) |
||
| scmatval.s | |- S = ( N ScMat R ) |
||
| Assertion | scmatscmid | |- ( ( N e. Fin /\ R e. V /\ M e. S ) -> E. c e. K M = ( c .x. .1. ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | scmatval.k | |- K = ( Base ` R ) |
|
| 2 | scmatval.a | |- A = ( N Mat R ) |
|
| 3 | scmatval.b | |- B = ( Base ` A ) |
|
| 4 | scmatval.1 | |- .1. = ( 1r ` A ) |
|
| 5 | scmatval.t | |- .x. = ( .s ` A ) |
|
| 6 | scmatval.s | |- S = ( N ScMat R ) |
|
| 7 | 1 2 3 4 5 6 | scmatel | |- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> ( M e. B /\ E. c e. K M = ( c .x. .1. ) ) ) ) |
| 8 | 7 | simplbda | |- ( ( ( N e. Fin /\ R e. V ) /\ M e. S ) -> E. c e. K M = ( c .x. .1. ) ) |
| 9 | 8 | 3impa | |- ( ( N e. Fin /\ R e. V /\ M e. S ) -> E. c e. K M = ( c .x. .1. ) ) |