Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tglngval.p | |
|
tglngval.l | |
||
tglngval.i | |
||
tglngval.g | |
||
tglngval.x | |
||
tglngval.y | |
||
tglngval.z | |
||
Assertion | tglngval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tglngval.p | |
|
2 | tglngval.l | |
|
3 | tglngval.i | |
|
4 | tglngval.g | |
|
5 | tglngval.x | |
|
6 | tglngval.y | |
|
7 | tglngval.z | |
|
8 | 1 2 3 | tglng | |
9 | 4 8 | syl | |
10 | 9 | oveqd | |
11 | 7 | necomd | |
12 | eldifsn | |
|
13 | 6 11 12 | sylanbrc | |
14 | 1 | fvexi | |
15 | 14 | rabex | |
16 | 15 | a1i | |
17 | oveq12 | |
|
18 | 17 | eleq2d | |
19 | simpl | |
|
20 | simpr | |
|
21 | 20 | oveq2d | |
22 | 19 21 | eleq12d | |
23 | 19 | oveq1d | |
24 | 20 23 | eleq12d | |
25 | 18 22 24 | 3orbi123d | |
26 | 25 | rabbidv | |
27 | sneq | |
|
28 | 27 | difeq2d | |
29 | eqid | |
|
30 | 26 28 29 | ovmpox | |
31 | 5 13 16 30 | syl3anc | |
32 | 10 31 | eqtrd | |