Step | Hyp | Ref
| Expression |
1 | | lines.b |
. . . . 5
β’ π΅ = (Baseβπ) |
2 | | lines.l |
. . . . 5
β’ πΏ = (LineMβπ) |
3 | | lines.s |
. . . . 5
β’ π = (Scalarβπ) |
4 | | lines.k |
. . . . 5
β’ πΎ = (Baseβπ) |
5 | | lines.p |
. . . . 5
β’ Β· = (
Β·π βπ) |
6 | | lines.a |
. . . . 5
β’ + =
(+gβπ) |
7 | | lines.m |
. . . . 5
β’ β =
(-gβπ) |
8 | | lines.1 |
. . . . 5
β’ 1 =
(1rβπ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | lines 46891 |
. . . 4
β’ (π β π β πΏ = (π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))})) |
10 | 9 | oveqd 7379 |
. . 3
β’ (π β π β (ππΏπ) = (π(π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))})π)) |
11 | 10 | adantr 482 |
. 2
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β (ππΏπ) = (π(π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))})π)) |
12 | | eqidd 2738 |
. . 3
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))}) = (π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))})) |
13 | | oveq2 7370 |
. . . . . . . 8
β’ (π₯ = π β (( 1 β π‘) Β· π₯) = (( 1 β π‘) Β· π)) |
14 | | oveq2 7370 |
. . . . . . . 8
β’ (π¦ = π β (π‘ Β· π¦) = (π‘ Β· π)) |
15 | 13, 14 | oveqan12d 7381 |
. . . . . . 7
β’ ((π₯ = π β§ π¦ = π) β ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦)) = ((( 1 β π‘) Β· π) + (π‘ Β· π))) |
16 | 15 | eqeq2d 2748 |
. . . . . 6
β’ ((π₯ = π β§ π¦ = π) β (π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦)) β π = ((( 1 β π‘) Β· π) + (π‘ Β· π)))) |
17 | 16 | rexbidv 3176 |
. . . . 5
β’ ((π₯ = π β§ π¦ = π) β (βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦)) β βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π)))) |
18 | 17 | rabbidv 3418 |
. . . 4
β’ ((π₯ = π β§ π¦ = π) β {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))} = {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))}) |
19 | 18 | adantl 483 |
. . 3
β’ (((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ (π₯ = π β§ π¦ = π)) β {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))} = {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))}) |
20 | | sneq 4601 |
. . . . 5
β’ (π₯ = π β {π₯} = {π}) |
21 | 20 | difeq2d 4087 |
. . . 4
β’ (π₯ = π β (π΅ β {π₯}) = (π΅ β {π})) |
22 | 21 | adantl 483 |
. . 3
β’ (((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β§ π₯ = π) β (π΅ β {π₯}) = (π΅ β {π})) |
23 | | simpr1 1195 |
. . 3
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β π΅) |
24 | | id 22 |
. . . . . . . 8
β’ (π β π β π β π) |
25 | 24 | necomd 3000 |
. . . . . . 7
β’ (π β π β π β π) |
26 | 25 | anim2i 618 |
. . . . . 6
β’ ((π β π΅ β§ π β π) β (π β π΅ β§ π β π)) |
27 | 26 | 3adant1 1131 |
. . . . 5
β’ ((π β π΅ β§ π β π΅ β§ π β π) β (π β π΅ β§ π β π)) |
28 | | eldifsn 4752 |
. . . . 5
β’ (π β (π΅ β {π}) β (π β π΅ β§ π β π)) |
29 | 27, 28 | sylibr 233 |
. . . 4
β’ ((π β π΅ β§ π β π΅ β§ π β π) β π β (π΅ β {π})) |
30 | 29 | adantl 483 |
. . 3
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β π β (π΅ β {π})) |
31 | 1 | fvexi 6861 |
. . . . 5
β’ π΅ β V |
32 | 31 | rabex 5294 |
. . . 4
β’ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))} β V |
33 | 32 | a1i 11 |
. . 3
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))} β V) |
34 | 12, 19, 22, 23, 30, 33 | ovmpodx 7511 |
. 2
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β (π(π₯ β π΅, π¦ β (π΅ β {π₯}) β¦ {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π₯) + (π‘ Β· π¦))})π) = {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))}) |
35 | 11, 34 | eqtrd 2777 |
1
β’ ((π β π β§ (π β π΅ β§ π β π΅ β§ π β π)) β (ππΏπ) = {π β π΅ β£ βπ‘ β πΎ π = ((( 1 β π‘) Β· π) + (π‘ Β· π))}) |