Metamath Proof Explorer


Theorem scmatscmid

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 ˙ = 1 A
scmatval.t · ˙ = A
scmatval.s S = N ScMat R
Assertion scmatscmid N Fin R V M S c K M = c · ˙ 1 ˙

Proof

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 ˙ = 1 A
5 scmatval.t · ˙ = A
6 scmatval.s S = N ScMat R
7 1 2 3 4 5 6 scmatel N Fin R V M S M B c K M = c · ˙ 1 ˙
8 7 simplbda N Fin R V M S c K M = c · ˙ 1 ˙
9 8 3impa N Fin R V M S c K M = c · ˙ 1 ˙