Step | Hyp | Ref
| Expression |
1 | | mat2pmatfval.t |
. 2
⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
2 | | df-mat2pmat 21470 |
. . . 4
⊢
matToPolyMat = (𝑛 ∈
Fin, 𝑟 ∈ V ↦
(𝑚 ∈
(Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))))) |
3 | 2 | a1i 11 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → matToPolyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))))) |
4 | | oveq12 7191 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑛 Mat 𝑟) = (𝑁 Mat 𝑅)) |
5 | 4 | fveq2d 6690 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = (Base‘(𝑁 Mat 𝑅))) |
6 | | mat2pmatfval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐴) |
7 | | mat2pmatfval.a |
. . . . . . . 8
⊢ 𝐴 = (𝑁 Mat 𝑅) |
8 | 7 | fveq2i 6689 |
. . . . . . 7
⊢
(Base‘𝐴) =
(Base‘(𝑁 Mat 𝑅)) |
9 | 6, 8 | eqtr2i 2763 |
. . . . . 6
⊢
(Base‘(𝑁 Mat
𝑅)) = 𝐵 |
10 | 5, 9 | eqtrdi 2790 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (Base‘(𝑛 Mat 𝑟)) = 𝐵) |
11 | | simpl 486 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → 𝑛 = 𝑁) |
12 | | 2fveq3 6691 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 →
(algSc‘(Poly1‘𝑟)) =
(algSc‘(Poly1‘𝑅))) |
13 | 12 | adantl 485 |
. . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
(algSc‘(Poly1‘𝑟)) =
(algSc‘(Poly1‘𝑅))) |
14 | | mat2pmatfval.s |
. . . . . . . . 9
⊢ 𝑆 = (algSc‘𝑃) |
15 | | mat2pmatfval.p |
. . . . . . . . . 10
⊢ 𝑃 = (Poly1‘𝑅) |
16 | 15 | fveq2i 6689 |
. . . . . . . . 9
⊢
(algSc‘𝑃) =
(algSc‘(Poly1‘𝑅)) |
17 | 14, 16 | eqtr2i 2763 |
. . . . . . . 8
⊢
(algSc‘(Poly1‘𝑅)) = 𝑆 |
18 | 13, 17 | eqtrdi 2790 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
(algSc‘(Poly1‘𝑟)) = 𝑆) |
19 | 18 | fveq1d 6688 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) →
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)) = (𝑆‘(𝑥𝑚𝑦))) |
20 | 11, 11, 19 | mpoeq123dv 7255 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦))) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) |
21 | 10, 20 | mpteq12dv 5125 |
. . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑟 = 𝑅) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
22 | 21 | adantl 485 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) ∧ (𝑛 = 𝑁 ∧ 𝑟 = 𝑅)) → (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑥 ∈ 𝑛, 𝑦 ∈ 𝑛 ↦
((algSc‘(Poly1‘𝑟))‘(𝑥𝑚𝑦)))) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
23 | | simpl 486 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑁 ∈ Fin) |
24 | | elex 3418 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
25 | 24 | adantl 485 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑅 ∈ V) |
26 | 6 | fvexi 6700 |
. . . 4
⊢ 𝐵 ∈ V |
27 | | mptexg 7006 |
. . . 4
⊢ (𝐵 ∈ V → (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) ∈ V) |
28 | 26, 27 | mp1i 13 |
. . 3
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦)))) ∈ V) |
29 | 3, 22, 23, 25, 28 | ovmpod 7329 |
. 2
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑁 matToPolyMat 𝑅) = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |
30 | 1, 29 | syl5eq 2786 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ (𝑆‘(𝑥𝑚𝑦))))) |