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