Metamath Proof Explorer


Theorem matsc

Description: The identity matrix multiplied with a scalar. (Contributed by Stefan O'Rear, 16-Jul-2018)

Ref Expression
Hypotheses matsc.a 𝐴 = ( 𝑁 Mat 𝑅 )
matsc.k 𝐾 = ( Base ‘ 𝑅 )
matsc.m · = ( ·𝑠𝐴 )
matsc.z 0 = ( 0g𝑅 )
Assertion matsc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 · ( 1r𝐴 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝐿 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 matsc.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 matsc.k 𝐾 = ( Base ‘ 𝑅 )
3 matsc.m · = ( ·𝑠𝐴 )
4 matsc.z 0 = ( 0g𝑅 )
5 simp3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → 𝐿𝐾 )
6 3simpa ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
7 1 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
8 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
9 eqid ( 1r𝐴 ) = ( 1r𝐴 )
10 8 9 ringidcl ( 𝐴 ∈ Ring → ( 1r𝐴 ) ∈ ( Base ‘ 𝐴 ) )
11 6 7 10 3syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 1r𝐴 ) ∈ ( Base ‘ 𝐴 ) )
12 eqid ( .r𝑅 ) = ( .r𝑅 )
13 eqid ( 𝑁 × 𝑁 ) = ( 𝑁 × 𝑁 )
14 1 8 2 3 12 13 matvsca2 ( ( 𝐿𝐾 ∧ ( 1r𝐴 ) ∈ ( Base ‘ 𝐴 ) ) → ( 𝐿 · ( 1r𝐴 ) ) = ( ( ( 𝑁 × 𝑁 ) × { 𝐿 } ) ∘f ( .r𝑅 ) ( 1r𝐴 ) ) )
15 5 11 14 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 · ( 1r𝐴 ) ) = ( ( ( 𝑁 × 𝑁 ) × { 𝐿 } ) ∘f ( .r𝑅 ) ( 1r𝐴 ) ) )
16 simp1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → 𝑁 ∈ Fin )
17 simp13 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝐿𝐾 )
18 fvex ( 1r𝑅 ) ∈ V
19 4 fvexi 0 ∈ V
20 18 19 ifex if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ∈ V
21 20 a1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) ∧ 𝑖𝑁𝑗𝑁 ) → if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ∈ V )
22 fconstmpo ( ( 𝑁 × 𝑁 ) × { 𝐿 } ) = ( 𝑖𝑁 , 𝑗𝑁𝐿 )
23 22 a1i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( ( 𝑁 × 𝑁 ) × { 𝐿 } ) = ( 𝑖𝑁 , 𝑗𝑁𝐿 ) )
24 eqid ( 1r𝑅 ) = ( 1r𝑅 )
25 1 24 4 mat1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐴 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) )
26 25 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 1r𝐴 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) )
27 16 16 17 21 23 26 offval22 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( ( ( 𝑁 × 𝑁 ) × { 𝐿 } ) ∘f ( .r𝑅 ) ( 1r𝐴 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝐿 ( .r𝑅 ) if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) ) )
28 ovif2 ( 𝐿 ( .r𝑅 ) if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) = if ( 𝑖 = 𝑗 , ( 𝐿 ( .r𝑅 ) ( 1r𝑅 ) ) , ( 𝐿 ( .r𝑅 ) 0 ) )
29 2 12 24 ringridm ( ( 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 ( .r𝑅 ) ( 1r𝑅 ) ) = 𝐿 )
30 29 3adant1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 ( .r𝑅 ) ( 1r𝑅 ) ) = 𝐿 )
31 2 12 4 ringrz ( ( 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 ( .r𝑅 ) 0 ) = 0 )
32 31 3adant1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 ( .r𝑅 ) 0 ) = 0 )
33 30 32 ifeq12d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → if ( 𝑖 = 𝑗 , ( 𝐿 ( .r𝑅 ) ( 1r𝑅 ) ) , ( 𝐿 ( .r𝑅 ) 0 ) ) = if ( 𝑖 = 𝑗 , 𝐿 , 0 ) )
34 28 33 eqtrid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 ( .r𝑅 ) if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) = if ( 𝑖 = 𝑗 , 𝐿 , 0 ) )
35 34 mpoeq3dv ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( 𝐿 ( .r𝑅 ) if ( 𝑖 = 𝑗 , ( 1r𝑅 ) , 0 ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝐿 , 0 ) ) )
36 15 27 35 3eqtrd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝐿𝐾 ) → ( 𝐿 · ( 1r𝐴 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝑗 , 𝐿 , 0 ) ) )