Theorem scmatel

Description: An N x N scalar matrix over (a ring) R . (Contributed 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	scmatel	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> ( M e. B /\ E. c e. K M = ( c .x. .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. = ( 1r ` A )
5		scmatval.t	|- .x. = ( .s ` A )
6		scmatval.s	|- S = ( N ScMat R )
7	1 2 3 4 5 6	scmatval	|- ( ( N e. Fin /\ R e. V ) -> S = { m e. B | E. c e. K m = ( c .x. .1. ) } )
8	7	eleq2d	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> M e. { m e. B | E. c e. K m = ( c .x. .1. ) } ) )
9		eqeq1	|- ( m = M -> ( m = ( c .x. .1. ) <-> M = ( c .x. .1. ) ) )
10	9	rexbidv	|- ( m = M -> ( E. c e. K m = ( c .x. .1. ) <-> E. c e. K M = ( c .x. .1. ) ) )
11	10	elrab	|- ( M e. { m e. B | E. c e. K m = ( c .x. .1. ) } <-> ( M e. B /\ E. c e. K M = ( c .x. .1. ) ) )
12	8 11	bitrdi	|- ( ( N e. Fin /\ R e. V ) -> ( M e. S <-> ( M e. B /\ E. c e. K M = ( c .x. .1. ) ) ) )