Metamath Proof Explorer

Theorem scmate

Description: An entry of an N x N scalar 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 )
scmate.k 
|- K = ( Base ` R )
scmate.0 
|- .0. = ( 0g ` R )
Assertion scmate 
|- ( ( ( 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 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
7 eqid 
 |-  ( .s ` A ) = ( .s ` A )
8 4 1 2 6 7 3 scmatscmid 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> E. c e. K M = ( c ( .s ` A ) ( 1r ` A ) ) )
9 oveq 
 |-  ( M = ( c ( .s ` A ) ( 1r ` A ) ) -> ( I M J ) = ( I ( c ( .s ` A ) ( 1r ` A ) ) J ) )
10 simpll1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> N e. Fin )
11 simpll2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> R e. Ring )
12 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> c e. K )
13 simplr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> ( I e. N /\ J e. N ) )
14 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. ) )
15 10 11 12 13 14 syl31anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> ( I ( c ( .s ` A ) ( 1r ` A ) ) J ) = if ( I = J , c , .0. ) )
16 9 15 sylan9eqr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) /\ M = ( c ( .s ` A ) ( 1r ` A ) ) ) -> ( I M J ) = if ( I = J , c , .0. ) )
17 16 ex 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) /\ c e. K ) -> ( M = ( c ( .s ` A ) ( 1r ` A ) ) -> ( I M J ) = if ( I = J , c , .0. ) ) )
18 17 reximdva 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. S ) /\ ( I e. N /\ J e. N ) ) -> ( E. c e. K M = ( c ( .s ` A ) ( 1r ` A ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) )
19 18 ex 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. S ) -> ( ( I e. N /\ J e. N ) -> ( E. c e. K M = ( c ( .s ` A ) ( 1r ` A ) ) -> E. c e. K ( I M J ) = if ( I = J , c , .0. ) ) ) )
20 8 19 mpid 
 |-  ( ( 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. ) ) )
21 20 imp 
 |-  ( ( ( 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. ) )