Step | Hyp | Ref
| Expression |
1 | | lngid 27431 |
. . 3
β’ LineG =
Slot (LineGβndx) |
2 | | fvex 6859 |
. . . 4
β’
(EEGβπ) β
V |
3 | 2 | a1i 11 |
. . 3
β’ (π β β β
(EEGβπ) β
V) |
4 | | eengstr 27978 |
. . . . 5
β’ (π β β β
(EEGβπ) Struct
β¨1, ;17β©) |
5 | | structn0fun 17031 |
. . . . 5
β’
((EEGβπ)
Struct β¨1, ;17β© β
Fun ((EEGβπ) β
{β
})) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π β β β Fun
((EEGβπ) β
{β
})) |
7 | | structcnvcnv 17033 |
. . . . . 6
β’
((EEGβπ)
Struct β¨1, ;17β© β
β‘β‘(EEGβπ) = ((EEGβπ) β {β
})) |
8 | 4, 7 | syl 17 |
. . . . 5
β’ (π β β β β‘β‘(EEGβπ) = ((EEGβπ) β {β
})) |
9 | 8 | funeqd 6527 |
. . . 4
β’ (π β β β (Fun
β‘β‘(EEGβπ) β Fun ((EEGβπ) β {β
}))) |
10 | 6, 9 | mpbird 257 |
. . 3
β’ (π β β β Fun β‘β‘(EEGβπ)) |
11 | | opex 5425 |
. . . . . 6
β’
β¨(LineGβndx), (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β V |
12 | 11 | prid2 4728 |
. . . . 5
β’
β¨(LineGβndx), (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©} |
13 | | elun2 4141 |
. . . . 5
β’
(β¨(LineGβndx), (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©} β
β¨(LineGβndx), (π₯
β (πΌβπ),
π¦ β
((πΌβπ) β
{π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©})) |
14 | 12, 13 | ax-mp 5 |
. . . 4
β’
β¨(LineGβndx), (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©}) |
15 | | eengv 27977 |
. . . 4
β’ (π β β β
(EEGβπ) =
({β¨(Baseβndx), (πΌβπ)β©, β¨(distβndx), (π₯ β (πΌβπ), π¦ β (πΌβπ) β¦ Ξ£π β (1...π)(((π₯βπ) β (π¦βπ))β2))β©} βͺ
{β¨(Itvβndx), (π₯
β (πΌβπ),
π¦ β
(πΌβπ) β¦
{π§ β
(πΌβπ) β£
π§ Btwn β¨π₯, π¦β©})β©, β¨(LineGβndx),
(π₯ β
(πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β©})) |
16 | 14, 15 | eleqtrrid 2841 |
. . 3
β’ (π β β β
β¨(LineGβndx), (π₯
β (πΌβπ),
π¦ β
((πΌβπ) β
{π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)})β© β (EEGβπ)) |
17 | | fvex 6859 |
. . . . 5
β’
(πΌβπ)
β V |
18 | 17 | difexi 5289 |
. . . . 5
β’
((πΌβπ)
β {π₯}) β
V |
19 | 17, 18 | mpoex 8016 |
. . . 4
β’ (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) β V |
20 | 19 | a1i 11 |
. . 3
β’ (π β β β (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) β V) |
21 | 1, 3, 10, 16, 20 | strfv2d 17082 |
. 2
β’ (π β β β (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) = (LineGβ(EEGβπ))) |
22 | | eengbas 27979 |
. . . 4
β’ (π β β β
(πΌβπ) =
(Baseβ(EEGβπ))) |
23 | | elntg.1 |
. . . 4
β’ π = (Baseβ(EEGβπ)) |
24 | 22, 23 | eqtr4di 2791 |
. . 3
β’ (π β β β
(πΌβπ) = π) |
25 | 24 | difeq1d 4085 |
. . . 4
β’ (π β β β
((πΌβπ) β
{π₯}) = (π β {π₯})) |
26 | 25 | adantr 482 |
. . 3
β’ ((π β β β§ π₯ β (πΌβπ)) β ((πΌβπ) β {π₯}) = (π β {π₯})) |
27 | 24 | adantr 482 |
. . . 4
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β (πΌβπ) = π) |
28 | | simpll 766 |
. . . . . 6
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π β β) |
29 | | elntg.2 |
. . . . . 6
β’ πΌ = (Itvβ(EEGβπ)) |
30 | | simplrl 776 |
. . . . . . 7
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π₯ β (πΌβπ)) |
31 | 28, 24 | syl 17 |
. . . . . . 7
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β (πΌβπ) = π) |
32 | 30, 31 | eleqtrd 2836 |
. . . . . 6
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π₯ β π) |
33 | | simplrr 777 |
. . . . . . . 8
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π¦ β ((πΌβπ) β {π₯})) |
34 | 33 | eldifad 3926 |
. . . . . . 7
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π¦ β (πΌβπ)) |
35 | 34, 31 | eleqtrd 2836 |
. . . . . 6
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π¦ β π) |
36 | | simpr 486 |
. . . . . . 7
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π§ β (πΌβπ)) |
37 | 36, 31 | eleqtrd 2836 |
. . . . . 6
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β π§ β π) |
38 | 28, 23, 29, 32, 35, 37 | ebtwntg 27980 |
. . . . 5
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β (π§ Btwn β¨π₯, π¦β© β π§ β (π₯πΌπ¦))) |
39 | 28, 23, 29, 37, 35, 32 | ebtwntg 27980 |
. . . . 5
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β (π₯ Btwn β¨π§, π¦β© β π₯ β (π§πΌπ¦))) |
40 | 28, 23, 29, 32, 37, 35 | ebtwntg 27980 |
. . . . 5
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β (π¦ Btwn β¨π₯, π§β© β π¦ β (π₯πΌπ§))) |
41 | 38, 39, 40 | 3orbi123d 1436 |
. . . 4
β’ (((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β§ π§ β (πΌβπ)) β ((π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©) β (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§)))) |
42 | 27, 41 | rabeqbidva 3422 |
. . 3
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π¦ β ((πΌβπ) β {π₯}))) β {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)} = {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))}) |
43 | 24, 26, 42 | mpoeq123dva 7435 |
. 2
β’ (π β β β (π₯ β (πΌβπ), π¦ β ((πΌβπ) β {π₯}) β¦ {π§ β (πΌβπ) β£ (π§ Btwn β¨π₯, π¦β© β¨ π₯ Btwn β¨π§, π¦β© β¨ π¦ Btwn β¨π₯, π§β©)}) = (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |
44 | 21, 43 | eqtr3d 2775 |
1
β’ (π β β β
(LineGβ(EEGβπ))
= (π₯ β π, π¦ β (π β {π₯}) β¦ {π§ β π β£ (π§ β (π₯πΌπ¦) β¨ π₯ β (π§πΌπ¦) β¨ π¦ β (π₯πΌπ§))})) |