Step | Hyp | Ref
| Expression |
1 | | scmatval.s |
. 2
⊢ 𝑆 = (𝑁 ScMat 𝑅) |
2 | | df-scmat 20116 |
. . . 4
⊢ ScMat =
(𝑛 ∈ Fin, 𝑟 ∈ V ↦
⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))}) |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → ScMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))})) |
4 | | ovex 6577 |
. . . . . 6
⊢ (𝑛 Mat 𝑟) ∈ V |
5 | 4 | a1i 11 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → (𝑛 Mat 𝑟) ∈ V) |
6 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑎 = (𝑛 Mat 𝑟) → (Base‘𝑎) = (Base‘(𝑛 Mat 𝑟))) |
7 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑛 Mat 𝑟) → (
·𝑠 ‘𝑎) = ( ·𝑠
‘(𝑛 Mat 𝑟))) |
8 | | eqidd 2611 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑛 Mat 𝑟) → 𝑐 = 𝑐) |
9 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑛 Mat 𝑟) → (1r‘𝑎) = (1r‘(𝑛 Mat 𝑟))) |
10 | 7, 8, 9 | oveq123d 6570 |
. . . . . . . . 9
⊢ (𝑎 = (𝑛 Mat 𝑟) → (𝑐( ·𝑠
‘𝑎)(1r‘𝑎)) = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))) |
11 | 10 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑎 = (𝑛 Mat 𝑟) → (𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎)) ↔ 𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))))) |
12 | 11 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑎 = (𝑛 Mat 𝑟) → (∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎)) ↔ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))))) |
13 | 6, 12 | rabeqbidv 3168 |
. . . . . 6
⊢ (𝑎 = (𝑛 Mat 𝑟) → {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))}) |
14 | 13 | adantl 481 |
. . . . 5
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) ∧ 𝑎 = (𝑛 Mat 𝑟)) → {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))}) |
15 | 5, 14 | csbied 3526 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} = {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))}) |
16 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
17 | 16 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅))) |
18 | | scmatval.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐴) |
19 | | scmatval.a |
. . . . . . . . 9
⊢ 𝐴 = (𝑁 Mat 𝑅) |
20 | 19 | fveq2i 6106 |
. . . . . . . 8
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
21 | 18, 20 | eqtri 2632 |
. . . . . . 7
⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅)) |
22 | 17, 21 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
23 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
24 | | scmatval.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
25 | 23, 24 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐾) |
26 | 25 | adantl 481 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘𝑟) = 𝐾) |
27 | 16 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (
·𝑠 ‘(𝑛 Mat 𝑟)) = ( ·𝑠
‘(𝑁 Mat 𝑅))) |
28 | | scmatval.t |
. . . . . . . . . . 11
⊢ · = (
·𝑠 ‘𝐴) |
29 | 19 | fveq2i 6106 |
. . . . . . . . . . 11
⊢ (
·𝑠 ‘𝐴) = ( ·𝑠
‘(𝑁 Mat 𝑅)) |
30 | 28, 29 | eqtri 2632 |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘(𝑁 Mat 𝑅)) |
31 | 27, 30 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (
·𝑠 ‘(𝑛 Mat 𝑟)) = · ) |
32 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑐 = 𝑐) |
33 | 16 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (1r‘(𝑛 Mat 𝑟)) = (1r‘(𝑁 Mat 𝑅))) |
34 | | scmatval.1 |
. . . . . . . . . . 11
⊢ 1 =
(1r‘𝐴) |
35 | 19 | fveq2i 6106 |
. . . . . . . . . . 11
⊢
(1r‘𝐴) = (1r‘(𝑁 Mat 𝑅)) |
36 | 34, 35 | eqtri 2632 |
. . . . . . . . . 10
⊢ 1 =
(1r‘(𝑁 Mat
𝑅)) |
37 | 33, 36 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (1r‘(𝑛 Mat 𝑟)) = 1 ) |
38 | 31, 32, 37 | oveq123d 6570 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) = (𝑐 · 1 )) |
39 | 38 | eqeq2d 2620 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) ↔ 𝑚 = (𝑐 · 1 ))) |
40 | 26, 39 | rexeqbidv 3130 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟))) ↔ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 ))) |
41 | 22, 40 | rabeqbidv 3168 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))} = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )}) |
42 | 41 | adantl 481 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → {𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘(𝑛 Mat 𝑟))(1r‘(𝑛 Mat 𝑟)))} = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )}) |
43 | 15, 42 | eqtrd 2644 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )}) |
44 | | simpl 472 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
45 | | elex 3185 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
46 | 45 | adantl 481 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V) |
47 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐴)
∈ V |
48 | 18, 47 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
49 | 48 | rabex 4740 |
. . . 4
⊢ {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )} ∈
V |
50 | 49 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )} ∈
V) |
51 | 3, 43, 44, 46, 50 | ovmpt2d 6686 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 ScMat 𝑅) = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )}) |
52 | 1, 51 | syl5eq 2656 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑆 = {𝑚 ∈ 𝐵 ∣ ∃𝑐 ∈ 𝐾 𝑚 = (𝑐 · 1 )}) |