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