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