Metamath Proof Explorer


Theorem legval

Description: Value of the less-than relationship. (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
Assertion legval φ˙=ef|xPyPf=x-˙yzPzxIye=x-˙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 elex G𝒢TarskiGV
7 simp1 p=Pd=-˙i=Ip=P
8 7 eqcomd p=Pd=-˙i=IP=p
9 simp2 p=Pd=-˙i=Id=-˙
10 9 eqcomd p=Pd=-˙i=I-˙=d
11 10 oveqd p=Pd=-˙i=Ix-˙y=xdy
12 11 eqeq2d p=Pd=-˙i=If=x-˙yf=xdy
13 simp3 p=Pd=-˙i=Ii=I
14 13 eqcomd p=Pd=-˙i=II=i
15 14 oveqd p=Pd=-˙i=IxIy=xiy
16 15 eleq2d p=Pd=-˙i=IzxIyzxiy
17 10 oveqd p=Pd=-˙i=Ix-˙z=xdz
18 17 eqeq2d p=Pd=-˙i=Ie=x-˙ze=xdz
19 16 18 anbi12d p=Pd=-˙i=IzxIye=x-˙zzxiye=xdz
20 8 19 rexeqbidv p=Pd=-˙i=IzPzxIye=x-˙zzpzxiye=xdz
21 12 20 anbi12d p=Pd=-˙i=If=x-˙yzPzxIye=x-˙zf=xdyzpzxiye=xdz
22 8 21 rexeqbidv p=Pd=-˙i=IyPf=x-˙yzPzxIye=x-˙zypf=xdyzpzxiye=xdz
23 8 22 rexeqbidv p=Pd=-˙i=IxPyPf=x-˙yzPzxIye=x-˙zxpypf=xdyzpzxiye=xdz
24 1 2 3 23 sbcie3s g=G[˙Baseg/p]˙[˙distg/d]˙[˙Itvg/i]˙xpypf=xdyzpzxiye=xdzxPyPf=x-˙yzPzxIye=x-˙z
25 24 opabbidv g=Gef|[˙Baseg/p]˙[˙distg/d]˙[˙Itvg/i]˙xpypf=xdyzpzxiye=xdz=ef|xPyPf=x-˙yzPzxIye=x-˙z
26 df-leg 𝒢=gVef|[˙Baseg/p]˙[˙distg/d]˙[˙Itvg/i]˙xpypf=xdyzpzxiye=xdz
27 2 fvexi -˙V
28 27 imaex -˙P×PV
29 p0ex V
30 28 29 unex -˙P×PV
31 30 a1i -˙P×PV
32 simprr xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙de=x-˙d
33 ovima0 xPdPx-˙d-˙P×P
34 33 ad5ant14 xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙dx-˙d-˙P×P
35 32 34 eqeltrd xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙de-˙P×P
36 simpllr xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙df=x-˙yzPzxIye=x-˙z
37 36 simpld xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙df=x-˙y
38 ovima0 xPyPx-˙y-˙P×P
39 38 ad3antrrr xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙dx-˙y-˙P×P
40 37 39 eqeltrd xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙df-˙P×P
41 35 40 jca xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙de-˙P×Pf-˙P×P
42 simprr xPyPf=x-˙yzPzxIye=x-˙zzPzxIye=x-˙z
43 eleq1w z=dzxIydxIy
44 oveq2 z=dx-˙z=x-˙d
45 44 eqeq2d z=de=x-˙ze=x-˙d
46 43 45 anbi12d z=dzxIye=x-˙zdxIye=x-˙d
47 46 cbvrexvw zPzxIye=x-˙zdPdxIye=x-˙d
48 42 47 sylib xPyPf=x-˙yzPzxIye=x-˙zdPdxIye=x-˙d
49 41 48 r19.29a xPyPf=x-˙yzPzxIye=x-˙ze-˙P×Pf-˙P×P
50 49 ex xPyPf=x-˙yzPzxIye=x-˙ze-˙P×Pf-˙P×P
51 50 rexlimivv xPyPf=x-˙yzPzxIye=x-˙ze-˙P×Pf-˙P×P
52 51 adantl xPyPf=x-˙yzPzxIye=x-˙ze-˙P×Pf-˙P×P
53 52 simpld xPyPf=x-˙yzPzxIye=x-˙ze-˙P×P
54 52 simprd xPyPf=x-˙yzPzxIye=x-˙zf-˙P×P
55 31 31 53 54 opabex2 ef|xPyPf=x-˙yzPzxIye=x-˙zV
56 55 mptru ef|xPyPf=x-˙yzPzxIye=x-˙zV
57 25 26 56 fvmpt GV𝒢G=ef|xPyPf=x-˙yzPzxIye=x-˙z
58 5 6 57 3syl φ𝒢G=ef|xPyPf=x-˙yzPzxIye=x-˙z
59 4 58 eqtrid φ˙=ef|xPyPf=x-˙yzPzxIye=x-˙z