Theorem legval 25479

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

Hypotheses

Ref	Expression
legval.p	|- P = ( Base ` G )
legval.d	|- .- = ( dist ` G )
legval.i	|- I = (Itv ` G )
legval.l	|- .<_ = (≤G ` G )
legval.g	|- ( ph -> G e. TarskiG )

Assertion

Ref	Expression
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 ) ) ) } )

Distinct variable groups:   e, f, G   x, y, z, I   x, e, y, z, P, f   .- , e, f, x, y, z

Allowed substitution hints:   ph( x, y, z, e, f)   G( x, y, z)   I( e, f)   .<_ ( x, y, z, e, f)

Proof of Theorem legval

Dummy variables d g i p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		legval.l	. 2 |- .<_ = (≤G ` G )
2		legval.g	. . 3 |- ( ph -> G e. TarskiG )
3		elex 3212	. . 3 |- ( G e. TarskiG -> G e. _V )
4		legval.p	. . . . . 6 |- P = ( Base ` G )
5		legval.d	. . . . . 6 |- .- = ( dist ` G )
6		legval.i	. . . . . 6 |- I = (Itv ` G )
7		simp1 1061	. . . . . . . 8 |- ( ( p = P /\ d = .- /\ i = I ) -> p = P )
8	7	eqcomd 2628	. . . . . . 7 |- ( ( p = P /\ d = .- /\ i = I ) -> P = p )
9		simp2 1062	. . . . . . . . . . . 12 |- ( ( p = P /\ d = .- /\ i = I ) -> d = .- )
10	9	eqcomd 2628	. . . . . . . . . . 11 |- ( ( p = P /\ d = .- /\ i = I ) -> .- = d )
11	10	oveqd 6667	. . . . . . . . . 10 |- ( ( p = P /\ d = .- /\ i = I ) -> ( x .- y ) = ( x d y ) )
12	11	eqeq2d 2632	. . . . . . . . 9 |- ( ( p = P /\ d = .- /\ i = I ) -> ( f = ( x .- y ) <-> f = ( x d y ) ) )
13		simp3 1063	. . . . . . . . . . . . . 14 |- ( ( p = P /\ d = .- /\ i = I ) -> i = I )
14	13	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ( p = P /\ d = .- /\ i = I ) -> I = i )
15	14	oveqd 6667	. . . . . . . . . . . 12 |- ( ( p = P /\ d = .- /\ i = I ) -> ( x I y ) = ( x i y ) )
16	15	eleq2d 2687	. . . . . . . . . . 11 |- ( ( p = P /\ d = .- /\ i = I ) -> ( z e. ( x I y ) <-> z e. ( x i y ) ) )
17	10	oveqd 6667	. . . . . . . . . . . 12 |- ( ( p = P /\ d = .- /\ i = I ) -> ( x .- z ) = ( x d z ) )
18	17	eqeq2d 2632	. . . . . . . . . . 11 |- ( ( p = P /\ d = .- /\ i = I ) -> ( e = ( x .- z ) <-> e = ( x d z ) ) )
19	16, 18	anbi12d 747	. . . . . . . . . 10 |- ( ( 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 3153	. . . . . . . . 9 |- ( ( 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 747	. . . . . . . 8 |- ( ( 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 3153	. . . . . . 7 |- ( ( 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 3153	. . . . . 6 |- ( ( 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	4, 5, 6, 23	sbcie3s 15917	. . . . 5 |- ( 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 4716	. . . 4 |- ( 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 25478	. . . 4 |- ≤G = ( 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		fvex 6201	. . . . . . . . . 10 |- ( dist ` G ) e. _V
28	5, 27	eqeltri 2697	. . . . . . . . 9 |- .- e. _V
29	28	imaex 7104	. . . . . . . 8 |- ( .- " ( P X. P ) ) e. _V
30		p0ex 4853	. . . . . . . 8 |- { (/) } e. _V
31	29, 30	unex 6956	. . . . . . 7 |- ( ( .- " ( P X. P ) ) u. { (/) } ) e. _V
32	31	a1i 11	. . . . . 6 |- ( T. -> ( ( .- " ( P X. P ) ) u. { (/) } ) e. _V )
33		simprr 796	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
34		ovima0 6813	. . . . . . . . . . . . . 14 |- ( ( x e. P /\ d e. P ) -> ( x .- d ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
35	34	ad5ant14 1302	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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. { (/) } ) )
36	33, 35	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ( ( ( ( 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. { (/) } ) )
37		simpllr 799	. . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) ) ) )
38	37	simpld 475	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
39		ovima0 6813	. . . . . . . . . . . . . 14 |- ( ( x e. P /\ y e. P ) -> ( x .- y ) e. ( ( .- " ( P X. P ) ) u. { (/) } ) )
40	39	ad3antrrr 766	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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. { (/) } ) )
41	38, 40	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ( ( ( ( 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. { (/) } ) )
42	36, 41	jca 554	. . . . . . . . . . 11 |- ( ( ( ( ( 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. { (/) } ) ) )
43		simprr 796	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
44		eleq1 2689	. . . . . . . . . . . . . 14 |- ( z = d -> ( z e. ( x I y ) <-> d e. ( x I y ) ) )
45		oveq2 6658	. . . . . . . . . . . . . . 15 |- ( z = d -> ( x .- z ) = ( x .- d ) )
46	45	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( z = d -> ( e = ( x .- z ) <-> e = ( x .- d ) ) )
47	44, 46	anbi12d 747	. . . . . . . . . . . . 13 |- ( z = d -> ( ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> ( d e. ( x I y ) /\ e = ( x .- d ) ) ) )
48	47	cbvrexv 3172	. . . . . . . . . . . 12 |- ( 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	43, 48	sylib 208	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
50	42, 49	r19.29a 3078	. . . . . . . . . 10 |- ( ( ( 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	ex 450	. . . . . . . . 9 |- ( ( 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. { (/) } ) ) ) )
52	51	rexlimivv 3036	. . . . . . . 8 |- ( 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	adantl 482	. . . . . . 7 |- ( ( 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. { (/) } ) ) )
54	53	simpld 475	. . . . . 6 |- ( ( 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. { (/) } ) )
55	53	simprd 479	. . . . . 6 |- ( ( 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. { (/) } ) )
56	32, 32, 54, 55	opabex2 7227	. . . . 5 |- ( 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 )
57	56	trud 1493	. . . 4 |- { <. 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
58	25, 26, 57	fvmpt 6282	. . 3 |- ( G e. _V -> (≤G ` 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	2, 3, 58	3syl 18	. 2 |- ( ph -> (≤G ` 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 ) ) ) } )
60	1, 59	syl5eq 2668	1 |- ( 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 ) ) ) } )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   T. wtru 1484   e. wcel 1990   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   u. cun 3572   (/)c0 3915   {csn 4177   {copab 4712   X. cxp 5112   "cima 5117   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Itvcitv 25335  ≤Gcleg 25477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-leg 25478

This theorem is referenced by:  legov  25480