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