Theorem scmatdmat

Description: A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	|- A = ( N Mat R )
	scmatid.b	|- B = ( Base ` A )
	scmatid.e	|- E = ( Base ` R )
	scmatid.0	|- .0. = ( 0g ` R )
	scmatid.s	|- S = ( N ScMat R )
	scmatdmat.d	|- D = ( N DMat R )
Assertion	scmatdmat	|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> M e. D ) )

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	|- A = ( N Mat R )
2		scmatid.b	|- B = ( Base ` A )
3		scmatid.e	|- E = ( Base ` R )
4		scmatid.0	|- .0. = ( 0g ` R )
5		scmatid.s	|- S = ( N ScMat R )
6		scmatdmat.d	|- D = ( N DMat R )
7		id	|- ( ( i m j ) = if ( i = j , c , .0. ) -> ( i m j ) = if ( i = j , c , .0. ) )
8		ifnefalse	|- ( i =/= j -> if ( i = j , c , .0. ) = .0. )
9	7 8	sylan9eq	|- ( ( ( i m j ) = if ( i = j , c , .0. ) /\ i =/= j ) -> ( i m j ) = .0. )
10	9	ex	|- ( ( i m j ) = if ( i = j , c , .0. ) -> ( i =/= j -> ( i m j ) = .0. ) )
11	10	a1i	|- ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. E ) /\ i e. N ) /\ j e. N ) -> ( ( i m j ) = if ( i = j , c , .0. ) -> ( i =/= j -> ( i m j ) = .0. ) ) )
12	11	ralimdva	|- ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. E ) /\ i e. N ) -> ( A. j e. N ( i m j ) = if ( i = j , c , .0. ) -> A. j e. N ( i =/= j -> ( i m j ) = .0. ) ) )
13	12	ralimdva	|- ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. E ) -> ( A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) -> A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) ) )
14	13	rexlimdva	|- ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) -> A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) ) )
15	14	ss2rabdv	|- ( ( N e. Fin /\ R e. Ring ) -> { m e. B | E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } C_ { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
16	15	adantr	|- ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> { m e. B | E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } C_ { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
17	1 2 5 3 4	scmatmats	|- ( ( N e. Fin /\ R e. Ring ) -> S = { m e. B | E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } )
18	1 2 4 6	dmatval	|- ( ( N e. Fin /\ R e. Ring ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
19	17 18	sseq12d	|- ( ( N e. Fin /\ R e. Ring ) -> ( S C_ D <-> { m e. B | E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } C_ { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
20	19	adantr	|- ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> ( S C_ D <-> { m e. B | E. c e. E A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } C_ { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
21	16 20	mpbird	|- ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> S C_ D )
22		simpr	|- ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> M e. S )
23	21 22	sseldd	|- ( ( ( N e. Fin /\ R e. Ring ) /\ M e. S ) -> M e. D )
24	23	ex	|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> M e. D ) )