Metamath Proof Explorer


Theorem tglngval

Description: The line going through points X and Y . (Contributed by Thierry Arnoux, 28-Mar-2019)

Ref Expression
Hypotheses tglngval.p P=BaseG
tglngval.l L=Line𝒢G
tglngval.i I=ItvG
tglngval.g φG𝒢Tarski
tglngval.x φXP
tglngval.y φYP
tglngval.z φXY
Assertion tglngval φXLY=zP|zXIYXzIYYXIz

Proof

Step Hyp Ref Expression
1 tglngval.p P=BaseG
2 tglngval.l L=Line𝒢G
3 tglngval.i I=ItvG
4 tglngval.g φG𝒢Tarski
5 tglngval.x φXP
6 tglngval.y φYP
7 tglngval.z φXY
8 1 2 3 tglng G𝒢TarskiL=xP,yPxzP|zxIyxzIyyxIz
9 4 8 syl φL=xP,yPxzP|zxIyxzIyyxIz
10 9 oveqd φXLY=XxP,yPxzP|zxIyxzIyyxIzY
11 7 necomd φYX
12 eldifsn YPXYPYX
13 6 11 12 sylanbrc φYPX
14 1 fvexi PV
15 14 rabex zP|zXIYXzIYYXIzV
16 15 a1i φzP|zXIYXzIYYXIzV
17 oveq12 x=Xy=YxIy=XIY
18 17 eleq2d x=Xy=YzxIyzXIY
19 simpl x=Xy=Yx=X
20 simpr x=Xy=Yy=Y
21 20 oveq2d x=Xy=YzIy=zIY
22 19 21 eleq12d x=Xy=YxzIyXzIY
23 19 oveq1d x=Xy=YxIz=XIz
24 20 23 eleq12d x=Xy=YyxIzYXIz
25 18 22 24 3orbi123d x=Xy=YzxIyxzIyyxIzzXIYXzIYYXIz
26 25 rabbidv x=Xy=YzP|zxIyxzIyyxIz=zP|zXIYXzIYYXIz
27 sneq x=Xx=X
28 27 difeq2d x=XPx=PX
29 eqid xP,yPxzP|zxIyxzIyyxIz=xP,yPxzP|zxIyxzIyyxIz
30 26 28 29 ovmpox XPYPXzP|zXIYXzIYYXIzVXxP,yPxzP|zxIyxzIyyxIzY=zP|zXIYXzIYYXIz
31 5 13 16 30 syl3anc φXxP,yPxzP|zxIyxzIyyxIzY=zP|zXIYXzIYYXIz
32 10 31 eqtrd φXLY=zP|zXIYXzIYYXIz