Step | Hyp | Ref
| Expression |
1 | | oveq2 7359 |
. . . 4
β’ (π = πΌ β (β βm π) = (β βm
πΌ)) |
2 | | rrnval.1 |
. . . 4
β’ π = (β βm
πΌ) |
3 | 1, 2 | eqtr4di 2795 |
. . 3
β’ (π = πΌ β (β βm π) = π) |
4 | | sumeq1 15533 |
. . . 4
β’ (π = πΌ β Ξ£π β π (((π₯βπ) β (π¦βπ))β2) = Ξ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) |
5 | 4 | fveq2d 6843 |
. . 3
β’ (π = πΌ β (ββΞ£π β π (((π₯βπ) β (π¦βπ))β2)) = (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
6 | 3, 3, 5 | mpoeq123dv 7426 |
. 2
β’ (π = πΌ β (π₯ β (β βm π), π¦ β (β βm π) β¦
(ββΞ£π
β π (((π₯βπ) β (π¦βπ))β2))) = (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)))) |
7 | | df-rrn 36223 |
. 2
β’
βn = (π β Fin β¦ (π₯ β (β βm π), π¦ β (β βm π) β¦
(ββΞ£π
β π (((π₯βπ) β (π¦βπ))β2)))) |
8 | | fvrn0 6869 |
. . . . 5
β’
(ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β (ran β βͺ
{β
}) |
9 | 8 | rgen2w 3067 |
. . . 4
β’
βπ₯ β
π βπ¦ β π (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β (ran β βͺ
{β
}) |
10 | | eqid 2737 |
. . . . 5
β’ (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) = (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) |
11 | 10 | fmpo 7992 |
. . . 4
β’
(βπ₯ β
π βπ¦ β π (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)) β (ran β βͺ
{β
}) β (π₯ β
π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆ(ran β βͺ
{β
})) |
12 | 9, 11 | mpbi 229 |
. . 3
β’ (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆ(ran β βͺ
{β
}) |
13 | | ovex 7384 |
. . . . 5
β’ (β
βm πΌ)
β V |
14 | 2, 13 | eqeltri 2834 |
. . . 4
β’ π β V |
15 | 14, 14 | xpex 7679 |
. . 3
β’ (π Γ π) β V |
16 | | cnex 11090 |
. . . . 5
β’ β
β V |
17 | | sqrtf 15208 |
. . . . . 6
β’
β:ββΆβ |
18 | | frn 6672 |
. . . . . 6
β’
(β:ββΆβ β ran β β
β) |
19 | 17, 18 | ax-mp 5 |
. . . . 5
β’ ran
β β β |
20 | 16, 19 | ssexi 5277 |
. . . 4
β’ ran
β β V |
21 | | p0ex 5337 |
. . . 4
β’ {β
}
β V |
22 | 20, 21 | unex 7672 |
. . 3
β’ (ran
β βͺ {β
}) β V |
23 | | fex2 7862 |
. . 3
β’ (((π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))):(π Γ π)βΆ(ran β βͺ {β
}) β§
(π Γ π) β V β§ (ran β
βͺ {β
}) β V) β (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) β V) |
24 | 12, 15, 22, 23 | mp3an 1461 |
. 2
β’ (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2))) β V |
25 | 6, 7, 24 | fvmpt 6945 |
1
β’ (πΌ β Fin β
(βnβπΌ) = (π₯ β π, π¦ β π β¦ (ββΞ£π β πΌ (((π₯βπ) β (π¦βπ))β2)))) |