Metamath Proof Explorer


Theorem legov

Description: Value of the less-than relationship. Definition 5.4 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019)

Ref Expression
Hypotheses legval.p P=BaseG
legval.d -˙=distG
legval.i I=ItvG
legval.l ˙=𝒢G
legval.g φG𝒢Tarski
legov.a φAP
legov.b φBP
legov.c φCP
legov.d φDP
Assertion legov φA-˙B˙C-˙DzPzCIDA-˙B=C-˙z

Proof

Step Hyp Ref Expression
1 legval.p P=BaseG
2 legval.d -˙=distG
3 legval.i I=ItvG
4 legval.l ˙=𝒢G
5 legval.g φG𝒢Tarski
6 legov.a φAP
7 legov.b φBP
8 legov.c φCP
9 legov.d φDP
10 1 2 3 4 5 legval φ˙=ef|xPyPf=x-˙yzPzxIye=x-˙z
11 10 breqd φA-˙B˙C-˙DA-˙Bef|xPyPf=x-˙yzPzxIye=x-˙zC-˙D
12 ovex A-˙BV
13 ovex C-˙DV
14 simpr e=A-˙Bf=C-˙Df=C-˙D
15 14 eqeq1d e=A-˙Bf=C-˙Df=x-˙yC-˙D=x-˙y
16 simpl e=A-˙Bf=C-˙De=A-˙B
17 16 eqeq1d e=A-˙Bf=C-˙De=x-˙zA-˙B=x-˙z
18 17 anbi2d e=A-˙Bf=C-˙DzxIye=x-˙zzxIyA-˙B=x-˙z
19 18 rexbidv e=A-˙Bf=C-˙DzPzxIye=x-˙zzPzxIyA-˙B=x-˙z
20 15 19 anbi12d e=A-˙Bf=C-˙Df=x-˙yzPzxIye=x-˙zC-˙D=x-˙yzPzxIyA-˙B=x-˙z
21 20 2rexbidv e=A-˙Bf=C-˙DxPyPf=x-˙yzPzxIye=x-˙zxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
22 eqid ef|xPyPf=x-˙yzPzxIye=x-˙z=ef|xPyPf=x-˙yzPzxIye=x-˙z
23 12 13 21 22 braba A-˙Bef|xPyPf=x-˙yzPzxIye=x-˙zC-˙DxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
24 11 23 bitrdi φA-˙B˙C-˙DxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
25 anass φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zφcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙z
26 25 anbi1i φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxPφcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxP
27 eqid 𝒢G=𝒢G
28 5 ad5antr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xG𝒢Tarski
29 28 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩G𝒢Tarski
30 simp-5r φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xcP
31 30 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩cP
32 simpllr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩xP
33 simp-4r φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xdP
34 33 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩dP
35 8 ad5antr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xCP
36 35 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩CP
37 simprl φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩zP
38 9 ad5antr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xDP
39 38 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩DP
40 simprr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩⟨“cdx”⟩𝒢G⟨“CDz”⟩
41 1 2 3 27 29 31 34 32 36 39 37 40 cgr3swap23 φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩⟨“cxd”⟩𝒢G⟨“CzD”⟩
42 simprl φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xxcId
43 42 adantr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩xcId
44 1 2 3 27 29 31 32 34 36 37 39 41 43 tgbtwnxfr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩zCID
45 simplrr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩A-˙B=c-˙x
46 1 2 3 27 29 31 32 34 36 37 39 41 cgr3simp1 φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩c-˙x=C-˙z
47 45 46 eqtrd φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩A-˙B=C-˙z
48 44 47 jca φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩zCIDA-˙B=C-˙z
49 eqid Line𝒢G=Line𝒢G
50 simplr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xxP
51 1 49 3 28 30 50 33 42 btwncolg3 φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xdcLine𝒢Gxc=x
52 simpllr φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xC-˙D=c-˙d
53 52 eqcomd φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xc-˙d=C-˙D
54 1 49 3 28 30 33 50 27 35 38 2 51 53 lnext φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzP⟨“cdx”⟩𝒢G⟨“CDz”⟩
55 48 54 reximddv φcPdPC-˙D=c-˙dxPxcIdA-˙B=c-˙xzPzCIDA-˙B=C-˙z
56 55 adantllr φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxPxcIdA-˙B=c-˙xzPzCIDA-˙B=C-˙z
57 26 56 sylanbr φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxPxcIdA-˙B=c-˙xzPzCIDA-˙B=C-˙z
58 simprr φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zzPzcIdA-˙B=c-˙z
59 eleq1w x=zxcIdzcId
60 oveq2 x=zc-˙x=c-˙z
61 60 eqeq2d x=zA-˙B=c-˙xA-˙B=c-˙z
62 59 61 anbi12d x=zxcIdA-˙B=c-˙xzcIdA-˙B=c-˙z
63 62 cbvrexvw xPxcIdA-˙B=c-˙xzPzcIdA-˙B=c-˙z
64 58 63 sylibr φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxPxcIdA-˙B=c-˙x
65 57 64 r19.29a φcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zzPzCIDA-˙B=C-˙z
66 65 adantl3r φxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙zcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zzPzCIDA-˙B=C-˙z
67 simpr φxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙zxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
68 oveq1 c=xc-˙d=x-˙d
69 68 eqeq2d c=xC-˙D=c-˙dC-˙D=x-˙d
70 oveq1 c=xcId=xId
71 70 eleq2d c=xzcIdzxId
72 oveq1 c=xc-˙z=x-˙z
73 72 eqeq2d c=xA-˙B=c-˙zA-˙B=x-˙z
74 71 73 anbi12d c=xzcIdA-˙B=c-˙zzxIdA-˙B=x-˙z
75 74 rexbidv c=xzPzcIdA-˙B=c-˙zzPzxIdA-˙B=x-˙z
76 69 75 anbi12d c=xC-˙D=c-˙dzPzcIdA-˙B=c-˙zC-˙D=x-˙dzPzxIdA-˙B=x-˙z
77 oveq2 d=yx-˙d=x-˙y
78 77 eqeq2d d=yC-˙D=x-˙dC-˙D=x-˙y
79 oveq2 d=yxId=xIy
80 79 eleq2d d=yzxIdzxIy
81 80 anbi1d d=yzxIdA-˙B=x-˙zzxIyA-˙B=x-˙z
82 81 rexbidv d=yzPzxIdA-˙B=x-˙zzPzxIyA-˙B=x-˙z
83 78 82 anbi12d d=yC-˙D=x-˙dzPzxIdA-˙B=x-˙zC-˙D=x-˙yzPzxIyA-˙B=x-˙z
84 76 83 cbvrex2vw cPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙zxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
85 67 84 sylibr φxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙zcPdPC-˙D=c-˙dzPzcIdA-˙B=c-˙z
86 66 85 r19.29vva φxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙zzPzCIDA-˙B=C-˙z
87 8 adantr φzPzCIDA-˙B=C-˙zCP
88 9 adantr φzPzCIDA-˙B=C-˙zDP
89 eqidd φzPzCIDA-˙B=C-˙zC-˙D=C-˙D
90 simpr φzPzCIDA-˙B=C-˙zzPzCIDA-˙B=C-˙z
91 oveq1 x=Cx-˙y=C-˙y
92 91 eqeq2d x=CC-˙D=x-˙yC-˙D=C-˙y
93 oveq1 x=CxIy=CIy
94 93 eleq2d x=CzxIyzCIy
95 oveq1 x=Cx-˙z=C-˙z
96 95 eqeq2d x=CA-˙B=x-˙zA-˙B=C-˙z
97 94 96 anbi12d x=CzxIyA-˙B=x-˙zzCIyA-˙B=C-˙z
98 97 rexbidv x=CzPzxIyA-˙B=x-˙zzPzCIyA-˙B=C-˙z
99 92 98 anbi12d x=CC-˙D=x-˙yzPzxIyA-˙B=x-˙zC-˙D=C-˙yzPzCIyA-˙B=C-˙z
100 oveq2 y=DC-˙y=C-˙D
101 100 eqeq2d y=DC-˙D=C-˙yC-˙D=C-˙D
102 oveq2 y=DCIy=CID
103 102 eleq2d y=DzCIyzCID
104 103 anbi1d y=DzCIyA-˙B=C-˙zzCIDA-˙B=C-˙z
105 104 rexbidv y=DzPzCIyA-˙B=C-˙zzPzCIDA-˙B=C-˙z
106 101 105 anbi12d y=DC-˙D=C-˙yzPzCIyA-˙B=C-˙zC-˙D=C-˙DzPzCIDA-˙B=C-˙z
107 99 106 rspc2ev CPDPC-˙D=C-˙DzPzCIDA-˙B=C-˙zxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
108 87 88 89 90 107 syl112anc φzPzCIDA-˙B=C-˙zxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙z
109 86 108 impbida φxPyPC-˙D=x-˙yzPzxIyA-˙B=x-˙zzPzCIDA-˙B=C-˙z
110 24 109 bitrd φA-˙B˙C-˙DzPzCIDA-˙B=C-˙z