Theorem scmateALT

Description: Alternate proof of scmate : An entry of an N x N scalar matrix over the ring R . This prove makes use of scmatmats but is longer and requires more distinct variables. (Contributed by AV, 19-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	scmatmat.a	|- A = ( N Mat R )
	scmatmat.b	|- B = ( Base ` A )
	scmatmat.s	|- S = ( N ScMat R )
	scmate.k	|- K = ( Base ` R )
	scmate.0	|- .0. = ( 0g ` R )
Assertion	scmateALT	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) )

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		scmate.k	|- K = ( Base ` R )
5		scmate.0	|- .0. = ( 0g ` R )
6	1 2 3 4 5	scmatmats	|- ( ( N e. Fin /\ R e. Ring ) -> S = { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } )
7	6	eleq2d	|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S <-> M e. { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } ) )
8		oveq	|- ( m = M -> ( i m j ) = ( i M j ) )
9	8	eqeq1d	|- ( m = M -> ( ( i m j ) = if ( i = j , c , .0. ) <-> ( i M j ) = if ( i = j , c , .0. ) ) )
10	9	2ralbidv	|- ( m = M -> ( 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 M j ) = if ( i = j , c , .0. ) ) )
11	10	rexbidv	|- ( m = M -> ( E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) <-> E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) ) )
12	11	elrab	|- ( M e. { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } <-> ( M e. B /\ E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) ) )
13		oveq1	|- ( i = I -> ( i M j ) = ( I M j ) )
14		eqeq1	|- ( i = I -> ( i = j <-> I = j ) )
15	14	ifbid	|- ( i = I -> if ( i = j , c , .0. ) = if ( I = j , c , .0. ) )
16	13 15	eqeq12d	|- ( i = I -> ( ( i M j ) = if ( i = j , c , .0. ) <-> ( I M j ) = if ( I = j , c , .0. ) ) )
17		oveq2	|- ( j = J -> ( I M j ) = ( I M J ) )
18		eqeq2	|- ( j = J -> ( I = j <-> I = J ) )
19	18	ifbid	|- ( j = J -> if ( I = j , c , .0. ) = if ( I = J , c , .0. ) )
20	17 19	eqeq12d	|- ( j = J -> ( ( I M j ) = if ( I = j , c , .0. ) <-> ( I M J ) = if ( I = J , c , .0. ) ) )
21	16 20	rspc2v	|- ( ( I e. N /\ J e. N ) -> ( A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) -> ( I M J ) = if ( I = J , c , .0. ) ) )
22	21	reximdv	|- ( ( I e. N /\ J e. N ) -> ( E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) )
23	22	com12	|- ( E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) )
24	23	adantl	|- ( ( M e. B /\ E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) ) -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) )
25	24	a1i	|- ( ( N e. Fin /\ R e. Ring ) -> ( ( M e. B /\ E. c e. K A. i e. N A. j e. N ( i M j ) = if ( i = j , c , .0. ) ) -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) ) )
26	12 25	syl5bi	|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) ) )
27	7 26	sylbid	|- ( ( N e. Fin /\ R e. Ring ) -> ( M e. S -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) ) )
28	27	ex	|- ( N e. Fin -> ( R e. Ring -> ( M e. S -> ( ( I e. N /\ J e. N ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) ) ) )
29	28	3imp1	|- ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) )