Step | Hyp | Ref
| Expression |
1 | | eqid 2730 |
. . . . 5
β’
[β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear |
2 | | fveq2 6892 |
. . . . . . . . 9
β’ (π = π β (πΌβπ) = (πΌβπ)) |
3 | 2 | eleq2d 2817 |
. . . . . . . 8
β’ (π = π β (π΄ β (πΌβπ) β π΄ β (πΌβπ))) |
4 | 2 | eleq2d 2817 |
. . . . . . . 8
β’ (π = π β (π΅ β (πΌβπ) β π΅ β (πΌβπ))) |
5 | 3, 4 | 3anbi12d 1435 |
. . . . . . 7
β’ (π = π β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅))) |
6 | 5 | anbi1d 628 |
. . . . . 6
β’ (π = π β (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
7 | 6 | rspcev 3613 |
. . . . 5
β’ ((π β β β§ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
8 | 1, 7 | mpanr2 700 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
9 | | simpr1 1192 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β π΄ β (πΌβπ)) |
10 | | simpr2 1193 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β π΅ β (πΌβπ)) |
11 | | colinearex 35334 |
. . . . . . . 8
β’ Colinear
β V |
12 | 11 | cnvex 7920 |
. . . . . . 7
β’ β‘ Colinear β V |
13 | | ecexg 8711 |
. . . . . . 7
β’ (β‘ Colinear β V β [β¨π΄, π΅β©]β‘ Colinear β V) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
β’
[β¨π΄, π΅β©]β‘ Colinear β V |
15 | | eleq1 2819 |
. . . . . . . . . 10
β’ (π = π΄ β (π β (πΌβπ) β π΄ β (πΌβπ))) |
16 | | neeq1 3001 |
. . . . . . . . . 10
β’ (π = π΄ β (π β π β π΄ β π)) |
17 | 15, 16 | 3anbi13d 1436 |
. . . . . . . . 9
β’ (π = π΄ β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π))) |
18 | | opeq1 4874 |
. . . . . . . . . . 11
β’ (π = π΄ β β¨π, πβ© = β¨π΄, πβ©) |
19 | 18 | eceq1d 8746 |
. . . . . . . . . 10
β’ (π = π΄ β [β¨π, πβ©]β‘ Colinear = [β¨π΄, πβ©]β‘ Colinear ) |
20 | 19 | eqeq2d 2741 |
. . . . . . . . 9
β’ (π = π΄ β (π = [β¨π, πβ©]β‘ Colinear β π = [β¨π΄, πβ©]β‘ Colinear )) |
21 | 17, 20 | anbi12d 629 |
. . . . . . . 8
β’ (π = π΄ β (((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ))) |
22 | 21 | rexbidv 3176 |
. . . . . . 7
β’ (π = π΄ β (βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ))) |
23 | | eleq1 2819 |
. . . . . . . . . 10
β’ (π = π΅ β (π β (πΌβπ) β π΅ β (πΌβπ))) |
24 | | neeq2 3002 |
. . . . . . . . . 10
β’ (π = π΅ β (π΄ β π β π΄ β π΅)) |
25 | 23, 24 | 3anbi23d 1437 |
. . . . . . . . 9
β’ (π = π΅ β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅))) |
26 | | opeq2 4875 |
. . . . . . . . . . 11
β’ (π = π΅ β β¨π΄, πβ© = β¨π΄, π΅β©) |
27 | 26 | eceq1d 8746 |
. . . . . . . . . 10
β’ (π = π΅ β [β¨π΄, πβ©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ) |
28 | 27 | eqeq2d 2741 |
. . . . . . . . 9
β’ (π = π΅ β (π = [β¨π΄, πβ©]β‘ Colinear β π = [β¨π΄, π΅β©]β‘ Colinear )) |
29 | 25, 28 | anbi12d 629 |
. . . . . . . 8
β’ (π = π΅ β (((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ))) |
30 | 29 | rexbidv 3176 |
. . . . . . 7
β’ (π = π΅ β (βπ β β ((π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π΄ β π) β§ π = [β¨π΄, πβ©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ))) |
31 | | eqeq1 2734 |
. . . . . . . . 9
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (π = [β¨π΄, π΅β©]β‘ Colinear β [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear )) |
32 | 31 | anbi2d 627 |
. . . . . . . 8
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ) β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
33 | 32 | rexbidv 3176 |
. . . . . . 7
β’ (π = [β¨π΄, π΅β©]β‘ Colinear β (βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ π = [β¨π΄, π΅β©]β‘ Colinear ) β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
34 | 22, 30, 33 | eloprabg 7522 |
. . . . . 6
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ [β¨π΄, π΅β©]β‘ Colinear β V) β
(β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
35 | 14, 34 | mp3an3 1448 |
. . . . 5
β’ ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ)) β (β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
36 | 9, 10, 35 | syl2anc 582 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β βπ β β ((π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅) β§ [β¨π΄, π΅β©]β‘ Colinear = [β¨π΄, π΅β©]β‘ Colinear ))) |
37 | 8, 36 | mpbird 256 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
38 | | df-ov 7416 |
. . . 4
β’ (π΄Lineπ΅) = (Lineββ¨π΄, π΅β©) |
39 | | df-br 5150 |
. . . . . 6
β’
(β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β
Line) |
40 | | df-line2 35411 |
. . . . . . 7
β’ Line =
{β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} |
41 | 40 | eleq2i 2823 |
. . . . . 6
β’
(β¨β¨π΄,
π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β Line β
β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
42 | 39, 41 | bitri 274 |
. . . . 5
β’
(β¨π΄, π΅β©Line[β¨π΄, π΅β©]β‘ Colinear β β¨β¨π΄, π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )}) |
43 | | funline 35416 |
. . . . . 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 2782 |
. . 3
β’
(β¨β¨π΄,
π΅β©, [β¨π΄, π΅β©]β‘ Colinear β© β {β¨β¨π, πβ©, πβ© β£ βπ β β ((π β (πΌβπ) β§ π β (πΌβπ) β§ π β π) β§ π = [β¨π, πβ©]β‘ Colinear )} β (π΄Lineπ΅) = [β¨π΄, π΅β©]β‘ Colinear ) |
48 | 37, 47 | syl 17 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = [β¨π΄, π΅β©]β‘ Colinear ) |
49 | | opex 5465 |
. . . 4
β’
β¨π΄, π΅β© β V |
50 | | dfec2 8710 |
. . . 4
β’
(β¨π΄, π΅β© β V β
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯}) |
51 | 49, 50 | ax-mp 5 |
. . 3
β’
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯} |
52 | | vex 3476 |
. . . . 5
β’ π₯ β V |
53 | 49, 52 | brcnv 5883 |
. . . 4
β’
(β¨π΄, π΅β©β‘ Colinear π₯ β π₯ Colinear β¨π΄, π΅β©) |
54 | 53 | abbii 2800 |
. . 3
β’ {π₯ β£ β¨π΄, π΅β©β‘ Colinear π₯} = {π₯ β£ π₯ Colinear β¨π΄, π΅β©} |
55 | 51, 54 | eqtri 2758 |
. 2
β’
[β¨π΄, π΅β©]β‘ Colinear = {π₯ β£ π₯ Colinear β¨π΄, π΅β©} |
56 | 48, 55 | eqtrdi 2786 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π΄ β π΅)) β (π΄Lineπ΅) = {π₯ β£ π₯ Colinear β¨π΄, π΅β©}) |