Theorem scmatmats

Description: The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatmat.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatmat.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatmat.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
	scmate.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	scmate.0	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	scmatmats	⊢ ( ( 𝑁 ∈ 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	scmatval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) } )
9		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → 𝑚 ∈ 𝐵 )
10	9	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → 𝑚 ∈ 𝐵 )
11		simpll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
12	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
13	2 6	ringidcl	⊢ ( 𝐴 ∈ Ring → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
14	12 13	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
15	14	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( 1r ‘ 𝐴 ) ∈ 𝐵 )
16	15	anim1ci	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑐 ∈ 𝐾 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) )
17	4 1 2 7	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑐 ∈ 𝐾 ∧ ( 1r ‘ 𝐴 ) ∈ 𝐵 ) ) → ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
18	11 16 17	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 )
19	1 2	eqmat	⊢ ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ∈ 𝐵 ) → ( 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) ) )
20	10 18 19	syl2anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) ) )
21		simplll	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → 𝑁 ∈ Fin )
22		simpllr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → 𝑅 ∈ Ring )
23		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → 𝑐 ∈ 𝐾 )
24	21 22 23	3jca	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾 ) )
25	1 4 5 6 7	scmatscmide	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) )
26	24 25	sylan	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) )
27	26	eqeq2d	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑖 𝑚 𝑗 ) = ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) ↔ ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
28	27	2ralbidva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = ( 𝑖 ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) 𝑗 ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
29	20 28	bitrd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝐾 ) → ( 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
30	29	rexbidva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑚 ∈ 𝐵 ) → ( ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) ↔ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) ) )
31	30	rabbidva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝐴 ) ( 1r ‘ 𝐴 ) ) } = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } )
32	8 31	eqtrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , 0 ) } )