Metamath Proof Explorer

Theorem scmatmats

Description: The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019) (Revised by AV, 19-Dec-2019)

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 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. ) } )

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 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
7 eqid 
 |-  ( .s ` A ) = ( .s ` A )
8 4 1 2 6 7 3 scmatval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S = { m e. B | E. c e. K m = ( c ( .s ` A ) ( 1r ` A ) ) } )
9 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> m e. B )
10 9 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> m e. B )
11 simpll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( N e. Fin /\ R e. Ring ) )
12 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
13 2 6 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. B )
14 12 13 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. B )
15 14 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( 1r ` A ) e. B )
16 15 anim1ci 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( c e. K /\ ( 1r ` A ) e. B ) )
17 4 1 2 7 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( c e. K /\ ( 1r ` A ) e. B ) ) -> ( c ( .s ` A ) ( 1r ` A ) ) e. B )
18 11 16 17 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( c ( .s ` A ) ( 1r ` A ) ) e. B )
19 1 2 eqmat 
 |-  ( ( m e. B /\ ( c ( .s ` A ) ( 1r ` A ) ) e. B ) -> ( m = ( c ( .s ` A ) ( 1r ` A ) ) <-> A. i e. N A. j e. N ( i m j ) = ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) ) )
20 10 18 19 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( m = ( c ( .s ` A ) ( 1r ` A ) ) <-> A. i e. N A. j e. N ( i m j ) = ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) ) )
21 simplll 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> N e. Fin )
22 simpllr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> R e. Ring )
23 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> c e. K )
24 21 22 23 3jca 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( N e. Fin /\ R e. Ring /\ c e. K ) )
25 1 4 5 6 7 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ c e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) = if ( i = j , c , .0. ) )
26 24 25 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) /\ ( i e. N /\ j e. N ) ) -> ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) = if ( i = j , c , .0. ) )
27 26 eqeq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) /\ ( i e. N /\ j e. N ) ) -> ( ( i m j ) = ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) <-> ( i m j ) = if ( i = j , c , .0. ) ) )
28 27 2ralbidva 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( A. i e. N A. j e. N ( i m j ) = ( i ( c ( .s ` A ) ( 1r ` A ) ) j ) <-> A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) ) )
29 20 28 bitrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) /\ c e. K ) -> ( m = ( c ( .s ` A ) ( 1r ` A ) ) <-> A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) ) )
30 29 rexbidva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ m e. B ) -> ( E. c e. K m = ( c ( .s ` A ) ( 1r ` A ) ) <-> E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) ) )
31 30 rabbidva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> { m e. B | E. c e. K m = ( c ( .s ` A ) ( 1r ` A ) ) } = { m e. B | E. c e. K A. i e. N A. j e. N ( i m j ) = if ( i = j , c , .0. ) } )
32 8 31 eqtrd 
 |-  ( ( 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. ) } )