Step | Hyp | Ref
| Expression |
1 | | mat2pmatfval.t |
. 2
β’ π = (π matToPolyMat π
) |
2 | | df-mat2pmat 22008 |
. . . 4
β’
matToPolyMat = (π β
Fin, π β V β¦
(π β
(Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦))))) |
3 | 2 | a1i 11 |
. . 3
β’ ((π β Fin β§ π
β π) β matToPolyMat = (π β Fin, π β V β¦ (π β (Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦)))))) |
4 | | oveq12 7360 |
. . . . . . 7
β’ ((π = π β§ π = π
) β (π Mat π) = (π Mat π
)) |
5 | 4 | fveq2d 6843 |
. . . . . 6
β’ ((π = π β§ π = π
) β (Baseβ(π Mat π)) = (Baseβ(π Mat π
))) |
6 | | mat2pmatfval.b |
. . . . . . 7
β’ π΅ = (Baseβπ΄) |
7 | | mat2pmatfval.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
8 | 7 | fveq2i 6842 |
. . . . . . 7
β’
(Baseβπ΄) =
(Baseβ(π Mat π
)) |
9 | 6, 8 | eqtr2i 2766 |
. . . . . 6
β’
(Baseβ(π Mat
π
)) = π΅ |
10 | 5, 9 | eqtrdi 2793 |
. . . . 5
β’ ((π = π β§ π = π
) β (Baseβ(π Mat π)) = π΅) |
11 | | simpl 483 |
. . . . . 6
β’ ((π = π β§ π = π
) β π = π) |
12 | | 2fveq3 6844 |
. . . . . . . . 9
β’ (π = π
β
(algScβ(Poly1βπ)) =
(algScβ(Poly1βπ
))) |
13 | 12 | adantl 482 |
. . . . . . . 8
β’ ((π = π β§ π = π
) β
(algScβ(Poly1βπ)) =
(algScβ(Poly1βπ
))) |
14 | | mat2pmatfval.s |
. . . . . . . . 9
β’ π = (algScβπ) |
15 | | mat2pmatfval.p |
. . . . . . . . . 10
β’ π = (Poly1βπ
) |
16 | 15 | fveq2i 6842 |
. . . . . . . . 9
β’
(algScβπ) =
(algScβ(Poly1βπ
)) |
17 | 14, 16 | eqtr2i 2766 |
. . . . . . . 8
β’
(algScβ(Poly1βπ
)) = π |
18 | 13, 17 | eqtrdi 2793 |
. . . . . . 7
β’ ((π = π β§ π = π
) β
(algScβ(Poly1βπ)) = π) |
19 | 18 | fveq1d 6841 |
. . . . . 6
β’ ((π = π β§ π = π
) β
((algScβ(Poly1βπ))β(π₯ππ¦)) = (πβ(π₯ππ¦))) |
20 | 11, 11, 19 | mpoeq123dv 7426 |
. . . . 5
β’ ((π = π β§ π = π
) β (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦))) = (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦)))) |
21 | 10, 20 | mpteq12dv 5194 |
. . . 4
β’ ((π = π β§ π = π
) β (π β (Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦)))) = (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦))))) |
22 | 21 | adantl 482 |
. . 3
β’ (((π β Fin β§ π
β π) β§ (π = π β§ π = π
)) β (π β (Baseβ(π Mat π)) β¦ (π₯ β π, π¦ β π β¦
((algScβ(Poly1βπ))β(π₯ππ¦)))) = (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦))))) |
23 | | simpl 483 |
. . 3
β’ ((π β Fin β§ π
β π) β π β Fin) |
24 | | elex 3461 |
. . . 4
β’ (π
β π β π
β V) |
25 | 24 | adantl 482 |
. . 3
β’ ((π β Fin β§ π
β π) β π
β V) |
26 | 6 | fvexi 6853 |
. . . 4
β’ π΅ β V |
27 | | mptexg 7167 |
. . . 4
β’ (π΅ β V β (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦)))) β V) |
28 | 26, 27 | mp1i 13 |
. . 3
β’ ((π β Fin β§ π
β π) β (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦)))) β V) |
29 | 3, 22, 23, 25, 28 | ovmpod 7501 |
. 2
β’ ((π β Fin β§ π
β π) β (π matToPolyMat π
) = (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦))))) |
30 | 1, 29 | eqtrid 2789 |
1
β’ ((π β Fin β§ π
β π) β π = (π β π΅ β¦ (π₯ β π, π¦ β π β¦ (πβ(π₯ππ¦))))) |