Theorem scmate

Description: An entry of an N x N scalar matrix over the ring R . (Contributed by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
	scmate.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmate.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	scmate	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
4		scmate.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
5		scmate.0	⊢ 0 = ( 0g ‘ 𝑅 )
6		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
7		eqid	⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ 𝐴 )
8	4 1 2 6 7 3	scmatscmid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ∃ 𝑐 ∈ 𝐾 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) )
9		oveq	⊢ ( 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) = ( 𝐼 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝐽 ) )
10		simpll1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → 𝑁 ∈ Fin )
11		simpll2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → 𝑅 ∈ Ring )
12		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → 𝑐 ∈ 𝐾 )
13		simplr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) )
14	1 4 5 6 7	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )
15	10 11 12 13 14	syl31anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝐼 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )
16	9 15	sylan9eqr	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) ∧ 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ) → ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )
17	16	ex	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
18	17	reximdva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ∃ 𝑐 ∈ 𝐾 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
19	18	ex	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ( ∃ 𝑐 ∈ 𝐾 𝑀 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) ) )
20	8 19	mpid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) → ( ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) ) )
21	20	imp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝑆 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ∃ 𝑐 ∈ 𝐾 ( 𝐼 𝑀 𝐽 ) = if ( 𝐼 = 𝐽 , 𝑐 , 0 ) )