Step | Hyp | Ref
| Expression |
1 | | fveq1 6842 |
. . . 4
β’ (π = π β (πβ1) = (πβ1)) |
2 | 1 | necon3i 2973 |
. . 3
β’ ((πβ1) β (πβ1) β π β π) |
3 | | rrx2line.i |
. . . 4
β’ πΌ = {1, 2} |
4 | | rrx2line.e |
. . . 4
β’ πΈ = (β^βπΌ) |
5 | | rrx2line.b |
. . . 4
β’ π = (β βm
πΌ) |
6 | | rrx2line.l |
. . . 4
β’ πΏ = (LineMβπΈ) |
7 | 3, 4, 5, 6 | rrx2line 46912 |
. . 3
β’ ((π β π β§ π β π β§ π β π) β (ππΏπ) = {π β π β£ βπ‘ β β ((πβ1) = (((1 β π‘) Β· (πβ1)) + (π‘ Β· (πβ1))) β§ (πβ2) = (((1 β π‘) Β· (πβ2)) + (π‘ Β· (πβ2))))}) |
8 | 2, 7 | syl3an3 1166 |
. 2
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (ππΏπ) = {π β π β£ βπ‘ β β ((πβ1) = (((1 β π‘) Β· (πβ1)) + (π‘ Β· (πβ1))) β§ (πβ2) = (((1 β π‘) Β· (πβ2)) + (π‘ Β· (πβ2))))}) |
9 | | reex 11147 |
. . . . . . . 8
β’ β
β V |
10 | | prex 5390 |
. . . . . . . . 9
β’ {1, 2}
β V |
11 | 3, 10 | eqeltri 2830 |
. . . . . . . 8
β’ πΌ β V |
12 | 9, 11 | elmap 8812 |
. . . . . . 7
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
13 | | id 22 |
. . . . . . . 8
β’ (π:πΌβΆβ β π:πΌβΆβ) |
14 | | 1ex 11156 |
. . . . . . . . . . 11
β’ 1 β
V |
15 | 14 | prid1 4724 |
. . . . . . . . . 10
β’ 1 β
{1, 2} |
16 | 15, 3 | eleqtrri 2833 |
. . . . . . . . 9
β’ 1 β
πΌ |
17 | 16 | a1i 11 |
. . . . . . . 8
β’ (π:πΌβΆβ β 1 β πΌ) |
18 | 13, 17 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π:πΌβΆβ β (πβ1) β β) |
19 | 12, 18 | sylbi 216 |
. . . . . 6
β’ (π β (β
βm πΌ)
β (πβ1) β
β) |
20 | 19, 5 | eleq2s 2852 |
. . . . 5
β’ (π β π β (πβ1) β β) |
21 | 20 | adantl 483 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ1) β β) |
22 | 9, 11 | elmap 8812 |
. . . . . . . 8
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
23 | | id 22 |
. . . . . . . . 9
β’ (π:πΌβΆβ β π:πΌβΆβ) |
24 | 16 | a1i 11 |
. . . . . . . . 9
β’ (π:πΌβΆβ β 1 β πΌ) |
25 | 23, 24 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π:πΌβΆβ β (πβ1) β β) |
26 | 22, 25 | sylbi 216 |
. . . . . . 7
β’ (π β (β
βm πΌ)
β (πβ1) β
β) |
27 | 26, 5 | eleq2s 2852 |
. . . . . 6
β’ (π β π β (πβ1) β β) |
28 | 27 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (πβ1) β β) |
29 | 28 | adantr 482 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ1) β β) |
30 | 9, 11 | elmap 8812 |
. . . . . . . 8
β’ (π β (β
βm πΌ)
β π:πΌβΆβ) |
31 | | id 22 |
. . . . . . . . 9
β’ (π:πΌβΆβ β π:πΌβΆβ) |
32 | 16 | a1i 11 |
. . . . . . . . 9
β’ (π:πΌβΆβ β 1 β πΌ) |
33 | 31, 32 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π:πΌβΆβ β (πβ1) β β) |
34 | 30, 33 | sylbi 216 |
. . . . . . 7
β’ (π β (β
βm πΌ)
β (πβ1) β
β) |
35 | 34, 5 | eleq2s 2852 |
. . . . . 6
β’ (π β π β (πβ1) β β) |
36 | 35 | 3ad2ant2 1135 |
. . . . 5
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (πβ1) β β) |
37 | 36 | adantr 482 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ1) β β) |
38 | | simpl3 1194 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ1) β (πβ1)) |
39 | | 2ex 12235 |
. . . . . . . . . . 11
β’ 2 β
V |
40 | 39 | prid2 4725 |
. . . . . . . . . 10
β’ 2 β
{1, 2} |
41 | 40, 3 | eleqtrri 2833 |
. . . . . . . . 9
β’ 2 β
πΌ |
42 | 41 | a1i 11 |
. . . . . . . 8
β’ (π:πΌβΆβ β 2 β πΌ) |
43 | 13, 42 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π:πΌβΆβ β (πβ2) β β) |
44 | 12, 43 | sylbi 216 |
. . . . . 6
β’ (π β (β
βm πΌ)
β (πβ2) β
β) |
45 | 44, 5 | eleq2s 2852 |
. . . . 5
β’ (π β π β (πβ2) β β) |
46 | 45 | adantl 483 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ2) β β) |
47 | 41 | a1i 11 |
. . . . . . . . 9
β’ (π:πΌβΆβ β 2 β πΌ) |
48 | 23, 47 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (π:πΌβΆβ β (πβ2) β β) |
49 | 22, 48 | sylbi 216 |
. . . . . . 7
β’ (π β (β
βm πΌ)
β (πβ2) β
β) |
50 | 49, 5 | eleq2s 2852 |
. . . . . 6
β’ (π β π β (πβ2) β β) |
51 | 50 | 3ad2ant1 1134 |
. . . . 5
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (πβ2) β β) |
52 | 51 | adantr 482 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ2) β β) |
53 | 5 | eleq2i 2826 |
. . . . . . . 8
β’ (π β π β π β (β βm πΌ)) |
54 | 53, 30 | bitri 275 |
. . . . . . 7
β’ (π β π β π:πΌβΆβ) |
55 | 41 | a1i 11 |
. . . . . . . 8
β’ (π:πΌβΆβ β 2 β πΌ) |
56 | 31, 55 | ffvelcdmd 7037 |
. . . . . . 7
β’ (π:πΌβΆβ β (πβ2) β β) |
57 | 54, 56 | sylbi 216 |
. . . . . 6
β’ (π β π β (πβ2) β β) |
58 | 57 | 3ad2ant2 1135 |
. . . . 5
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (πβ2) β β) |
59 | 58 | adantr 482 |
. . . 4
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (πβ2) β β) |
60 | | rrx2linesl.s |
. . . 4
β’ π = (((πβ2) β (πβ2)) / ((πβ1) β (πβ1))) |
61 | 21, 29, 37, 38, 46, 52, 59, 60 | affinecomb1 46874 |
. . 3
β’ (((π β π β§ π β π β§ (πβ1) β (πβ1)) β§ π β π) β (βπ‘ β β ((πβ1) = (((1 β π‘) Β· (πβ1)) + (π‘ Β· (πβ1))) β§ (πβ2) = (((1 β π‘) Β· (πβ2)) + (π‘ Β· (πβ2)))) β (πβ2) = ((π Β· ((πβ1) β (πβ1))) + (πβ2)))) |
62 | 61 | rabbidva 3413 |
. 2
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β {π β π β£ βπ‘ β β ((πβ1) = (((1 β π‘) Β· (πβ1)) + (π‘ Β· (πβ1))) β§ (πβ2) = (((1 β π‘) Β· (πβ2)) + (π‘ Β· (πβ2))))} = {π β π β£ (πβ2) = ((π Β· ((πβ1) β (πβ1))) + (πβ2))}) |
63 | 8, 62 | eqtrd 2773 |
1
β’ ((π β π β§ π β π β§ (πβ1) β (πβ1)) β (ππΏπ) = {π β π β£ (πβ2) = ((π Β· ((πβ1) β (πβ1))) + (πβ2))}) |