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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatscmide.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
scmatscmide.0 ⊢ 0 = ( 0g ‘ 𝑅 )
scmatscmide.1 ⊢ 1 = ( 1r ‘ 𝐴 )
scmatscmide.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
Assertion scmatscmide ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐶 ∗ 1 ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝐶 , 0 ) )

Proof

Step Hyp Ref Expression
1 scmatscmide.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 scmatscmide.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 scmatscmide.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 scmatscmide.1 ⊢ 1 = ( 1r ‘ 𝐴 )
5 scmatscmide.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
6 simpl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
7 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
8 1 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
10 9 4 ringidcl ⊢ ( 𝐴 ∈ Ring → 1 ∈ ( Base ‘ 𝐴 ) )
11 8 10 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 1 ∈ ( Base ‘ 𝐴 ) )
12 11 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝐴 ) )
13 7 12 jca ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) )
14 13 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐶 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) )
15 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 1 9 2 5 16 matvscacell ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝐴 ) ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐶 ∗ 1 ) 𝐽 ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐼 1 𝐽 ) ) )
18 6 14 15 17 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐶 ∗ 1 ) 𝐽 ) = ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐼 1 𝐽 ) ) )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 simpl1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
21 simprl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
22 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
23 1 19 3 20 6 21 22 4 mat1ov ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 1 𝐽 ) = if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) )
24 23 oveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 𝐼 1 𝐽 ) ) = ( 𝐶 ( .r ‘ 𝑅 ) if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) ) )
25 ovif2 ⊢ ( 𝐶 ( .r ‘ 𝑅 ) if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝐼 = 𝐽 , ( 𝐶 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝐶 ( .r ‘ 𝑅 ) 0 ) )
26 2 16 19 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝐶 )
27 26 3adant1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝐶 )
28 2 16 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( .r ‘ 𝑅 ) 0 ) = 0 )
29 28 3adant1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( .r ‘ 𝑅 ) 0 ) = 0 )
30 27 29 ifeq12d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → if ( 𝐼 = 𝐽 , ( 𝐶 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) , ( 𝐶 ( .r ‘ 𝑅 ) 0 ) ) = if ( 𝐼 = 𝐽 , 𝐶 , 0 ) )
31 25 30 syl5eq ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) → ( 𝐶 ( .r ‘ 𝑅 ) if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝐼 = 𝐽 , 𝐶 , 0 ) )
32 31 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐶 ( .r ‘ 𝑅 ) if ( 𝐼 = 𝐽 , ( 1r ‘ 𝑅 ) , 0 ) ) = if ( 𝐼 = 𝐽 , 𝐶 , 0 ) )
33 18 24 32 3eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐶 ∗ 1 ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝐶 , 0 ) )