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	eqtrid	⊢ ( ( 𝑁 ∈ 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 ) )