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 = ( Base ` G )
legval.d 
|- .- = ( dist ` G )
legval.i 
|- I = ( Itv ` G )
legval.l 
|- .<_ = ( leG ` G )
legval.g 
|- ( ph -> G e. TarskiG )
Assertion legval 
|- ( ph -> .<_ = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )

Proof

Step Hyp Ref Expression
1 legval.p 
 |-  P = ( Base ` G )
2 legval.d 
 |-  .- = ( dist ` G )
3 legval.i 
 |-  I = ( Itv ` G )
4 legval.l 
 |-  .<_ = ( leG ` G )
5 legval.g 
 |-  ( ph -> G e. TarskiG )
6 elex 
 |-  ( G e. TarskiG -> G e. _V )
7 simp1 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> p = P )
8 7 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> P = p )
9 simp2 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> d = .- )
10 9 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> .- = d )
11 10 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x .- y ) = ( x d y ) )
12 11 eqeq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( f = ( x .- y ) <-> f = ( x d y ) ) )
13 simp3 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> i = I )
14 13 eqcomd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> I = i )
15 14 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x I y ) = ( x i y ) )
16 15 eleq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( z e. ( x I y ) <-> z e. ( x i y ) ) )
17 10 oveqd 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( x .- z ) = ( x d z ) )
18 17 eqeq2d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( e = ( x .- z ) <-> e = ( x d z ) ) )
19 16 18 anbi12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> ( z e. ( x i y ) /\ e = ( x d z ) ) ) )
20 8 19 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) )
21 12 20 anbi12d 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) <-> ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) ) )
22 8 21 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) <-> E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) ) )
23 8 22 rexeqbidv 
 |-  ( ( p = P /\ d = .- /\ i = I ) -> ( E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) <-> E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) ) )
24 1 2 3 23 sbcie3s 
 |-  ( g = G -> ( [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) <-> E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) )
25 24 opabbidv 
 |-  ( g = G -> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )
26 df-leg 
 |-  leG = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. ( Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )
27 2 fvexi 
 |-  .- e. _V
28 27 imaex 
 |-  ( .- " ( P X. P ) ) e. _V
29 p0ex 
 |-  { (/) } e. _V
30 28 29 unex 
 |-  ( ( .- " ( P X. P ) ) u. { (/) } ) e. _V
31 30 a1i 
 |-  ( T. -> ( ( .- " ( P X. P ) ) u. { (/) } ) e. _V )
32 simprr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> e = ( x .- d ) )
33 ovima0 
 |-  ( ( x e. P /\ d e. P ) -> ( x .- d ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
34 33 ad5ant14 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> ( x .- d ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
35 32 34 eqeltrd 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> e e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
36 simpllr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) )
37 36 simpld 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> f = ( x .- y ) )
38 ovima0 
 |-  ( ( x e. P /\ y e. P ) -> ( x .- y ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
39 38 ad3antrrr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> ( x .- y ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
40 37 39 eqeltrd 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> f e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
41 35 40 jca 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) /\ d e. P ) /\ ( d e. ( x I y ) /\ e = ( x .- d ) ) ) -> ( e e. ( ( .- " ( P X. P ) ) u. { (/) } ) /\ f e. ( ( .- " ( P X. P ) ) u. { (/) } ) ) )
42 simprr 
 |-  ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) )
43 eleq1w 
 |-  ( z = d -> ( z e. ( x I y ) <-> d e. ( x I y ) ) )
44 oveq2 
 |-  ( z = d -> ( x .- z ) = ( x .- d ) )
45 44 eqeq2d 
 |-  ( z = d -> ( e = ( x .- z ) <-> e = ( x .- d ) ) )
46 43 45 anbi12d 
 |-  ( z = d -> ( ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> ( d e. ( x I y ) /\ e = ( x .- d ) ) ) )
47 46 cbvrexvw 
 |-  ( E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> E. d e. P ( d e. ( x I y ) /\ e = ( x .- d ) ) )
48 42 47 sylib 
 |-  ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> E. d e. P ( d e. ( x I y ) /\ e = ( x .- d ) ) )
49 41 48 r19.29a 
 |-  ( ( ( x e. P /\ y e. P ) /\ ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> ( e e. ( ( .- " ( P X. P ) ) u. { (/) } ) /\ f e. ( ( .- " ( P X. P ) ) u. { (/) } ) ) )
50 49 ex 
 |-  ( ( x e. P /\ y e. P ) -> ( ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) -> ( e e. ( ( .- " ( P X. P ) ) u. { (/) } ) /\ f e. ( ( .- " ( P X. P ) ) u. { (/) } ) ) ) )
51 50 rexlimivv 
 |-  ( E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) -> ( e e. ( ( .- " ( P X. P ) ) u. { (/) } ) /\ f e. ( ( .- " ( P X. P ) ) u. { (/) } ) ) )
52 51 adantl 
 |-  ( ( T. /\ E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> ( e e. ( ( .- " ( P X. P ) ) u. { (/) } ) /\ f e. ( ( .- " ( P X. P ) ) u. { (/) } ) ) )
53 52 simpld 
 |-  ( ( T. /\ E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> e e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
54 52 simprd 
 |-  ( ( T. /\ E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) ) -> f e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
55 31 31 53 54 opabex2 
 |-  ( T. -> { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } e. _V )
56 55 mptru 
 |-  { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } e. _V
57 25 26 56 fvmpt 
 |-  ( G e. _V -> ( leG ` G ) = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )
58 5 6 57 3syl 
 |-  ( ph -> ( leG ` G ) = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )
59 4 58 eqtrid 
 |-  ( ph -> .<_ = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )