Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
[β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear |
2 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π β (πΌβπ) = (πΌβπ)) |
3 | 2 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π β (π΄ β (πΌβπ) β π΄ β (πΌβπ))) |
4 | 2 | eleq2d 2820 |
. . . . . . . 8
β’ (π = π β (π΅ β (πΌβπ) β π΅ β (πΌβπ))) |
5 | 3, 4 | 3anbi12d 1438 |
. . . . . . 7
β’ (π = π β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅))) |
6 | 5 | anbi1d 631 |
. . . . . 6
β’ (π = π β (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
7 | 6 | rspcev 3613 |
. . . . 5
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
8 | 1, 7 | mpanr2 703 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
9 | | simpr1 1195 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β π΄ β (πΌβπ)) |
10 | | simpr2 1196 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β π΅ β (πΌβπ)) |
11 | | colinearex 35063 |
. . . . . . . 8
β’ Colinear
β V |
12 | 11 | cnvex 7916 |
. . . . . . 7
β’ β‘ Colinear β V |
13 | | ecexg 8707 |
. . . . . . 7
β’ (β‘ Colinear β V β [β¨π΄, π΅β©]β‘ Colinear β V) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
β’
[β¨π΄, π΅β©]β‘ Colinear β V |
15 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = π΄ β (π β (πΌβπ) β π΄ β (πΌβπ))) |
16 | | neeq1 3004 |
. . . . . . . . . 10
β’ (π = π΄ β (π β π β π΄ β π)) |
17 | 15, 16 | 3anbi13d 1439 |
. . . . . . . . 9
β’ (π = π΄ β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π))) |
18 | | opeq1 4874 |
. . . . . . . . . . 11
β’ (π = π΄ β β¨π, πβ© = β¨π΄, πβ©) |
19 | 18 | eceq1d 8742 |
. . . . . . . . . 10
β’ (π = π΄ β [β¨π, πβ©]β‘ Colinear = [β¨π΄, πβ©]β‘ Colinear ) |
20 | 19 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π΄ β (π = [β¨π, πβ©]β‘ Colinear β π = [β¨π΄, πβ©]β‘ Colinear )) |
21 | 17, 20 | anbi12d 632 |
. . . . . . . 8
β’ (π = π΄ β (((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ))) |
22 | 21 | rexbidv 3179 |
. . . . . . 7
β’ (π = π΄ β (βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ))) |
23 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = π΅ β (π β (πΌβπ) β π΅ β (πΌβπ))) |
24 | | neeq2 3005 |
. . . . . . . . . 10
β’ (π = π΅ β (π΄ β π β π΄ β π΅)) |
25 | 23, 24 | 3anbi23d 1440 |
. . . . . . . . 9
β’ (π = π΅ β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅))) |
26 | | opeq2 4875 |
. . . . . . . . . . 11
β’ (π = π΅ β β¨π΄, πβ© = β¨π΄, π΅β©) |
27 | 26 | eceq1d 8742 |
. . . . . . . . . 10
β’ (π = π΅ β [β¨π΄, πβ©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ) |
28 | 27 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π΅ β (π = [β¨π΄, πβ©]β‘ Colinear β π = [β¨π΄, π΅β©]β‘ Colinear )) |
29 | 25, 28 | anbi12d 632 |
. . . . . . . 8
β’ (π = π΅ β (((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ))) |
30 | 29 | rexbidv 3179 |
. . . . . . 7
β’ (π = π΅ β (βπ β β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ))) |
31 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (π = [β¨π΄, π΅β©]β‘ Colinear β [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
32 | 31 | anbi2d 630 |
. . . . . . . 8
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
33 | 32 | rexbidv 3179 |
. . . . . . 7
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
34 | 22, 30, 33 | eloprabg 7518 |
. . . . . 6
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ [β¨π΄, π΅β©]β‘ Colinear β V) β
(β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
35 | 14, 34 | mp3an3 1451 |
. . . . 5
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
36 | 9, 10, 35 | syl2anc 585 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
37 | 8, 36 | mpbird 257 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
38 | | df-ov 7412 |
. . . 4
β’ (π΄Lineπ΅) = (Lineββ¨π΄, π΅β©) |
39 | | df-br 5150 |
. . . . . 6
β’
(β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β
Line) |
40 | | df-line2 35140 |
. . . . . . 7
β’ Line =
{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} |
41 | 40 | eleq2i 2826 |
. . . . . 6
β’
(β¨β¨π΄,
π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β Line β
β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
42 | 39, 41 | bitri 275 |
. . . . 5
β’
(β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
43 | | funline 35145 |
. . . . . 6
β’ Fun
Line |
44 | | funbrfv 6943 |
. . . . . 6
β’ (Fun Line
β (β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β (Lineββ¨π΄, π΅β©) = [β¨π΄, π΅β©]β‘ Colinear )) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
β’
(β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β (Lineββ¨π΄, π΅β©) = [β¨π΄, π΅β©]β‘ Colinear ) |
46 | 42, 45 | sylbir 234 |
. . . 4
β’
(β¨β¨π΄,
π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β (Lineββ¨π΄, π΅β©) = [β¨π΄, π΅β©]β‘ Colinear ) |
47 | 38, 46 | eqtrid 2785 |
. . 3
β’
(β¨β¨π΄,
π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β (π΄Lineπ΅) = [β¨π΄, π΅β©]β‘ Colinear ) |
48 | 37, 47 | syl 17 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = [β¨π΄, π΅β©]β‘ Colinear ) |
49 | | opex 5465 |
. . . 4
β’
β¨π΄, π΅β© β V |
50 | | dfec2 8706 |
. . . 4
β’
(β¨π΄, π΅β© β V β
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯}) |
51 | 49, 50 | ax-mp 5 |
. . 3
β’
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯} |
52 | | vex 3479 |
. . . . 5
β’ π₯ β V |
53 | 49, 52 | brcnv 5883 |
. . . 4
β’
(β¨π΄, π΅β©β‘ Colinear π₯ β π₯ Colinear β¨π΄, π΅β©) |
54 | 53 | abbii 2803 |
. . 3
β’ {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯} = {π₯ β£ π₯ Colinear β¨π΄, π΅β©} |
55 | 51, 54 | eqtri 2761 |
. 2
β’
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ π₯ Colinear β¨π΄, π΅β©} |
56 | 48, 55 | eqtrdi 2789 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β£ π₯ Colinear β¨π΄, π΅β©}) |