Metamath Proof Explorer

Theorem scmatval

Description: The set of N x N scalar matrices over (a ring) R . (Contributed by AV, 18-Dec-2019)

Ref Expression
Hypotheses scmatval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
scmatval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
scmatval.1 ⊢ 1 = ( 1r ‘ 𝐴 )
scmatval.t ⊢ · = ( ·𝑠 ‘ 𝐴 )
scmatval.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion scmatval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )

Proof

Step Hyp Ref Expression
1 scmatval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 scmatval.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3 scmatval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 scmatval.1 ⊢ 1 = ( 1r ‘ 𝐴 )
5 scmatval.t ⊢ · = ( ·𝑠 ‘ 𝐴 )
6 scmatval.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
7 df-scmat ⊢ ScMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } )
8 7 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ScMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } ) )
9 ovexd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ( 𝑛 Mat 𝑟 ) ∈ V )
10 fveq2 ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( Base ‘ 𝑎 ) = ( Base ‘ ( 𝑛 Mat 𝑟 ) ) )
11 fveq2 ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( ·𝑠 ‘ 𝑎 ) = ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) )
12 eqidd ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → 𝑐 = 𝑐 )
13 fveq2 ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( 1r ‘ 𝑎 ) = ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) )
14 11 12 13 oveq123d ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) )
15 14 eqeq2d ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) ↔ 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) ) )
16 15 rexbidv ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) ) )
17 10 16 rabeqbidv ⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } = { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) } )
18 17 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) ∧ 𝑎 = ( 𝑛 Mat 𝑟 ) ) → { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } = { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) } )
19 9 18 csbied ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } = { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) } )
20 oveq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
21 20 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
22 2 fveq2i ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
23 3 22 eqtri ⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
24 21 23 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
25 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
26 25 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐾 )
27 26 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ 𝑟 ) = 𝐾 )
28 20 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑅 ) ) )
29 2 fveq2i ⊢ ( ·𝑠 ‘ 𝐴 ) = ( ·𝑠 ‘ ( 𝑁 Mat 𝑅 ) )
30 5 29 eqtri ⊢ · = ( ·𝑠 ‘ ( 𝑁 Mat 𝑅 ) )
31 28 30 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) = · )
32 eqidd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑐 = 𝑐 )
33 20 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) ) )
34 2 fveq2i ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
35 4 34 eqtri ⊢ 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
36 33 35 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) = 1 )
37 31 32 36 oveq123d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) = ( 𝑐 · 1 ) )
38 37 eqeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) ↔ 𝑚 = ( 𝑐 · 1 ) ) )
39 27 38 rexeqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) ↔ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) ) )
40 24 39 rabeqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) } = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )
41 40 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ ( 𝑛 Mat 𝑟 ) ) ( 1r ‘ ( 𝑛 Mat 𝑟 ) ) ) } = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )
42 19 41 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )
43 simpl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
44 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
45 44 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ V )
46 3 fvexi ⊢ 𝐵 ∈ V
47 46 rabex ⊢ { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } ∈ V
48 47 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } ∈ V )
49 8 42 43 45 48 ovmpod ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 ScMat 𝑅 ) = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )
50 6 49 syl5eq ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑆 = { 𝑚 ∈ 𝐵 ∣ ∃ 𝑐 ∈ 𝐾 𝑚 = ( 𝑐 · 1 ) } )