Metamath Proof Explorer

Theorem scmatscmide

Description: An entry of a scalar matrix expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019)

Ref Expression
Hypotheses scmatscmide.a 
|- A = ( N Mat R )
scmatscmide.b 
|- B = ( Base ` R )
scmatscmide.0 
|- .0. = ( 0g ` R )
scmatscmide.1 
|- .1. = ( 1r ` A )
scmatscmide.m 
|- .* = ( .s ` A )
Assertion scmatscmide 
|- ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( C .* .1. ) J ) = if ( I = J , C , .0. ) )

Proof

Step Hyp Ref Expression
1 scmatscmide.a 
 |-  A = ( N Mat R )
2 scmatscmide.b 
 |-  B = ( Base ` R )
3 scmatscmide.0 
 |-  .0. = ( 0g ` R )
4 scmatscmide.1 
 |-  .1. = ( 1r ` A )
5 scmatscmide.m 
 |-  .* = ( .s ` A )
6 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> R e. Ring )
7 simp3 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> C e. B )
8 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
9 eqid 
 |-  ( Base ` A ) = ( Base ` A )
10 9 4 ringidcl 
 |-  ( A e. Ring -> .1. e. ( Base ` A ) )
11 8 10 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` A ) )
12 11 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> .1. e. ( Base ` A ) )
13 7 12 jca 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> ( C e. B /\ .1. e. ( Base ` A ) ) )
14 13 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( C e. B /\ .1. e. ( Base ` A ) ) )
15 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I e. N /\ J e. N ) )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 1 9 2 5 16 matvscacell 
 |-  ( ( R e. Ring /\ ( C e. B /\ .1. e. ( Base ` A ) ) /\ ( I e. N /\ J e. N ) ) -> ( I ( C .* .1. ) J ) = ( C ( .r ` R ) ( I .1. J ) ) )
18 6 14 15 17 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( C .* .1. ) J ) = ( C ( .r ` R ) ( I .1. J ) ) )
19 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
20 simpl1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> N e. Fin )
21 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> I e. N )
22 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> J e. N )
23 1 19 3 20 6 21 22 4 mat1ov 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I .1. J ) = if ( I = J , ( 1r ` R ) , .0. ) )
24 23 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( C ( .r ` R ) ( I .1. J ) ) = ( C ( .r ` R ) if ( I = J , ( 1r ` R ) , .0. ) ) )
25 ovif2 
 |-  ( C ( .r ` R ) if ( I = J , ( 1r ` R ) , .0. ) ) = if ( I = J , ( C ( .r ` R ) ( 1r ` R ) ) , ( C ( .r ` R ) .0. ) )
26 2 16 19 ringridm 
 |-  ( ( R e. Ring /\ C e. B ) -> ( C ( .r ` R ) ( 1r ` R ) ) = C )
27 26 3adant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> ( C ( .r ` R ) ( 1r ` R ) ) = C )
28 2 16 3 ringrz 
 |-  ( ( R e. Ring /\ C e. B ) -> ( C ( .r ` R ) .0. ) = .0. )
29 28 3adant1 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> ( C ( .r ` R ) .0. ) = .0. )
30 27 29 ifeq12d 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> if ( I = J , ( C ( .r ` R ) ( 1r ` R ) ) , ( C ( .r ` R ) .0. ) ) = if ( I = J , C , .0. ) )
31 25 30 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring /\ C e. B ) -> ( C ( .r ` R ) if ( I = J , ( 1r ` R ) , .0. ) ) = if ( I = J , C , .0. ) )
32 31 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( C ( .r ` R ) if ( I = J , ( 1r ` R ) , .0. ) ) = if ( I = J , C , .0. ) )
33 18 24 32 3eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ C e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( C .* .1. ) J ) = if ( I = J , C , .0. ) )