Step | Hyp | Ref
| Expression |
1 | | mat2pmatfval.t |
. 2
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
2 | | df-mat2pmat 20512 |
. . . 4
⊢
matToPolyMat = (𝑛 ∈
Fin, 𝑟 ∈ V ↦
(𝑚 ∈
(Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))) |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))) |
4 | | oveq12 6659 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
5 | 4 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅))) |
6 | | mat2pmatfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
7 | | mat2pmatfval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
8 | 7 | fveq2i 6194 |
. . . . . . 7
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
9 | 6, 8 | eqtr2i 2645 |
. . . . . 6
⊢
(Base‘(𝑁 Mat
𝑅)) = 𝐵 |
10 | 5, 9 | syl6eq 2672 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
11 | | simpl 473 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
12 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Poly1‘𝑟) =
(Poly1‘𝑅)) |
13 | 12 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(algSc‘(Poly1‘𝑟)) =
(algSc‘(Poly1‘𝑅))) |
14 | 13 | adantl 482 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
(algSc‘(Poly1‘𝑟)) =
(algSc‘(Poly1‘𝑅))) |
15 | | mat2pmatfval.s |
. . . . . . . . 9
⊢ 𝑆 = (algSc‘𝑃) |
16 | | mat2pmatfval.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
17 | 16 | fveq2i 6194 |
. . . . . . . . 9
⊢
(algSc‘𝑃) =
(algSc‘(Poly1‘𝑅)) |
18 | 15, 17 | eqtr2i 2645 |
. . . . . . . 8
⊢
(algSc‘(Poly1‘𝑅)) = 𝑆 |
19 | 14, 18 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
(algSc‘(Poly1‘𝑟)) = 𝑆) |
20 | 19 | fveq1d 6193 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)) = (𝑆‘(𝑥𝑚𝑦))) |
21 | 11, 11, 20 | mpt2eq123dv 6717 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) |
22 | 10, 21 | mpteq12dv 4733 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
23 | 22 | adantl 482 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
24 | | simpl 473 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
25 | | elex 3212 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
26 | 25 | adantl 482 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V) |
27 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝐴)
∈ V |
28 | 6, 27 | eqeltri 2697 |
. . . 4
⊢ 𝐵 ∈ V |
29 | | mptexg 6484 |
. . . 4
⊢ (𝐵 ∈ V → (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) ∈ V) |
30 | 28, 29 | mp1i 13 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) ∈ V) |
31 | 3, 23, 24, 26, 30 | ovmpt2d 6788 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 matToPolyMat 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
32 | 1, 31 | syl5eq 2668 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |