Step | Hyp | Ref
| Expression |
1 | | fveq2 6843 |
. . . . 5
β’ (π = π β (πΌβπ) = (πΌβπ)) |
2 | 1 | opeq2d 4838 |
. . . 4
β’ (π = π β β¨(Baseβndx),
(πΌβπ)β© =
β¨(Baseβndx), (πΌβπ)β©) |
3 | 1 | adantr 482 |
. . . . . 6
β’ ((π = π β§ π₯ β (πΌβπ)) β (πΌβπ) = (πΌβπ)) |
4 | | simpl 484 |
. . . . . . . 8
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β π = π) |
5 | 4 | oveq2d 7374 |
. . . . . . 7
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (1...π) = (1...π)) |
6 | 5 | sumeq1d 15591 |
. . . . . 6
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2) = Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2)) |
7 | 1, 3, 6 | mpoeq123dva 7432 |
. . . . 5
β’ (π = π β (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2)) = (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))) |
8 | 7 | opeq2d 4838 |
. . . 4
β’ (π = π β β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β© = β¨(distβndx),
(π₯ β
(πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©) |
9 | 2, 8 | preq12d 4703 |
. . 3
β’ (π = π β {β¨(Baseβndx),
(πΌβπ)β©,
β¨(distβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} = {β¨(Baseβndx),
(πΌβπ)β©,
β¨(distβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©}) |
10 | 1 | adantr 482 |
. . . . . . 7
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β (πΌβπ) = (πΌβπ)) |
11 | 10 | rabeqdv 3421 |
. . . . . 6
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β (πΌβπ))) β {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©} = {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©}) |
12 | 1, 3, 11 | mpoeq123dva 7432 |
. . . . 5
β’ (π = π β (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©}) = (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})) |
13 | 12 | opeq2d 4838 |
. . . 4
β’ (π = π β β¨(Itvβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})β© = β¨(Itvβndx),
(π₯ β
(πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})β©) |
14 | 3 | difeq1d 4082 |
. . . . . 6
β’ ((π = π β§ π₯ β (πΌβπ)) β ((πΌβπ) β {π₯}) = ((πΌβπ) β {π₯})) |
15 | 1 | rabeqdv 3421 |
. . . . . . 7
β’ (π = π β {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)} = {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((π = π β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)} = {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) |
17 | 1, 14, 16 | mpoeq123dva 7432 |
. . . . 5
β’ (π = π β (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) = (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})) |
18 | 17 | opeq2d 4838 |
. . . 4
β’ (π = π β β¨(LineGβndx), (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© = β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©) |
19 | 13, 18 | preq12d 4703 |
. . 3
β’ (π = π β {β¨(Itvβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©} = {β¨(Itvβndx),
(π₯ β
(πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©}) |
20 | 9, 19 | uneq12d 4125 |
. 2
β’ (π = π β ({β¨(Baseβndx),
(πΌβπ)β©,
β¨(distβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©}) = ({β¨(Baseβndx),
(πΌβπ)β©,
β¨(distβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©})) |
21 | | df-eeng 27969 |
. 2
β’ EEG =
(π β β β¦
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©})) |
22 | | prex 5390 |
. . 3
β’
{β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} β V |
23 | | prex 5390 |
. . 3
β’
{β¨(Itvβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ {π§ β (πΌβπ) β£ π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©} β V |
24 | 22, 23 | unex 7681 |
. 2
β’
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©}) β V |
25 | 20, 21, 24 | fvmpt 6949 |
1
β’ (π β β β
(EEGβπ) =
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©})) |