Theorem scmatmat

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

	Ref	Expression
Hypotheses	scmatmat.a	|- A = ( N Mat R )
	scmatmat.b	|- B = ( Base ` A )
	scmatmat.s	|- S = ( N ScMat R )
Assertion	scmatmat	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S -> M e. B ) )

Proof

Step	Hyp	Ref	Expression
1		scmatmat.a	|- A = ( N Mat R )
2		scmatmat.b	|- B = ( Base ` A )
3		scmatmat.s	|- S = ( N ScMat R )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5		eqid	|- ( 1r ` A ) = ( 1r ` A )
6		eqid	|- ( .s ` A ) = ( .s ` A )
7	4 1 2 5 6 3	scmatel	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> ( M e. B /\ E. c e. ( Base ` R ) M = ( c ( .s ` A ) ( 1r ` A ) ) ) ) )
8		simpl	|- ( ( M e. B /\ E. c e. ( Base ` R ) M = ( c ( .s ` A ) ( 1r ` A ) ) ) -> M e. B )
9	7 8	biimtrdi	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S -> M e. B ) )