Metamath Proof Explorer

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