Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttgval Structured version   Unicode version

Theorem ttgval 23870
 Description: Define a function to augment a complex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.)
Hypotheses
Ref Expression
ttgval.n toTG
ttgval.b
ttgval.m
ttgval.s
ttgval.i Itv
Assertion
Ref Expression
ttgval sSet Itv sSet LineG
Distinct variable groups:   ,,,   ,,,   ,,,,   ,,,   , ,,   , ,,
Allowed substitution hints:   ()   ()   (,,,)   (,,,)   ()   ()

Proof of Theorem ttgval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ttgval.n . . . . 5 toTG
21a1i 11 . . . 4 toTG
3 elex 3122 . . . . 5
4 fveq2 5865 . . . . . . . . . 10
5 ttgval.b . . . . . . . . . 10
64, 5syl6eqr 2526 . . . . . . . . 9
7 fveq2 5865 . . . . . . . . . . . . . 14
8 ttgval.m . . . . . . . . . . . . . 14
97, 8syl6eqr 2526 . . . . . . . . . . . . 13
109oveqd 6300 . . . . . . . . . . . 12
11 fveq2 5865 . . . . . . . . . . . . . 14
12 ttgval.s . . . . . . . . . . . . . 14
1311, 12syl6eqr 2526 . . . . . . . . . . . . 13
14 eqidd 2468 . . . . . . . . . . . . 13
159oveqd 6300 . . . . . . . . . . . . 13
1613, 14, 15oveq123d 6304 . . . . . . . . . . . 12
1710, 16eqeq12d 2489 . . . . . . . . . . 11
1817rexbidv 2973 . . . . . . . . . 10
196, 18rabeqbidv 3108 . . . . . . . . 9
206, 6, 19mpt2eq123dv 6342 . . . . . . . 8
2120csbeq1d 3442 . . . . . . 7 sSet Itv sSet LineG sSet Itv sSet LineG
22 oveq1 6290 . . . . . . . . 9 sSet Itv sSet Itv
23 rabeq 3107 . . . . . . . . . . . 12
246, 23syl 16 . . . . . . . . . . 11
256, 6, 24mpt2eq123dv 6342 . . . . . . . . . 10
2625opeq2d 4220 . . . . . . . . 9 LineG LineG
2722, 26oveq12d 6301 . . . . . . . 8 sSet Itv sSet LineG sSet Itv sSet LineG
2827csbeq2dv 3835 . . . . . . 7 sSet Itv sSet LineG sSet Itv sSet LineG
2921, 28eqtrd 2508 . . . . . 6 sSet Itv sSet LineG sSet Itv sSet LineG
30 df-ttg 23869 . . . . . 6 toTG sSet Itv sSet LineG
31 ovex 6308 . . . . . . 7 sSet Itv sSet LineG
3231csbex 4580 . . . . . 6 sSet Itv sSet LineG
3329, 30, 32fvmpt 5949 . . . . 5 toTG sSet Itv sSet LineG
343, 33syl 16 . . . 4 toTG sSet Itv sSet LineG
35 fvex 5875 . . . . . . . 8
365, 35eqeltri 2551 . . . . . . 7
3736, 36mpt2ex 6860 . . . . . 6
3837a1i 11 . . . . 5
39 simpr 461 . . . . . . 7
40 oveq2 6291 . . . . . . . . . . 11
41 oveq2 6291 . . . . . . . . . . . 12
4241oveq2d 6299 . . . . . . . . . . 11
4340, 42eqeq12d 2489 . . . . . . . . . 10
4443rexbidv 2973 . . . . . . . . 9
4544rabbidv 3105 . . . . . . . 8
46 oveq1 6290 . . . . . . . . . . . . 13
4746oveq2d 6299 . . . . . . . . . . . 12
4847eqeq2d 2481 . . . . . . . . . . 11
4948rexbidv 2973 . . . . . . . . . 10
5049rabbidv 3105 . . . . . . . . 9
51 oveq1 6290 . . . . . . . . . . . . 13
5251eqeq1d 2469 . . . . . . . . . . . 12
5352rexbidv 2973 . . . . . . . . . . 11
5453cbvrabv 3112 . . . . . . . . . 10
5554a1i 11 . . . . . . . . 9
5650, 55eqtrd 2508 . . . . . . . 8
5745, 56cbvmpt2v 6360 . . . . . . 7
5839, 57syl6eqr 2526 . . . . . 6
59 simpr 461 . . . . . . . . . 10
6059, 57syl6eq 2524 . . . . . . . . 9
6160opeq2d 4220 . . . . . . . 8 Itv Itv
6261oveq2d 6299 . . . . . . 7 sSet Itv sSet Itv
6360oveqd 6300 . . . . . . . . . . . . 13
6463eleq2d 2537 . . . . . . . . . . . 12
6560oveqd 6300 . . . . . . . . . . . . 13
6665eleq2d 2537 . . . . . . . . . . . 12
6760oveqd 6300 . . . . . . . . . . . . 13
6867eleq2d 2537 . . . . . . . . . . . 12
6964, 66, 683orbi123d 1298 . . . . . . . . . . 11
7069rabbidv 3105 . . . . . . . . . 10
71703ad2ant1 1017 . . . . . . . . 9
7271mpt2eq3dva 6344 . . . . . . . 8
7372opeq2d 4220 . . . . . . 7 LineG LineG
7462, 73oveq12d 6301 . . . . . 6 sSet Itv sSet LineG sSet Itv sSet LineG
7558, 74syldan 470 . . . . 5 sSet Itv sSet LineG sSet Itv sSet LineG
7638, 75csbied 3462 . . . 4 sSet Itv sSet LineG sSet Itv sSet LineG
772, 34, 763eqtrd 2512 . . 3 sSet Itv sSet LineG
7877fveq2d 5869 . . . . . . . . . . . . 13 Itv Itv sSet Itv sSet LineG
79 itvid 23582 . . . . . . . . . . . . . 14 Itv Slot Itv
80 1nn0 10810 . . . . . . . . . . . . . . . . . 18
81 6nn 10696 . . . . . . . . . . . . . . . . . 18
8280, 81decnncl 10988 . . . . . . . . . . . . . . . . 17 ;
8382nnrei 10544 . . . . . . . . . . . . . . . 16 ;
84 6nn0 10815 . . . . . . . . . . . . . . . . 17
85 7nn 10697 . . . . . . . . . . . . . . . . 17
86 6lt7 10716 . . . . . . . . . . . . . . . . 17
8780, 84, 85, 86declt 10996 . . . . . . . . . . . . . . . 16 ; ;
8883, 87ltneii 9696 . . . . . . . . . . . . . . 15 ; ;
89 itvndx 23580 . . . . . . . . . . . . . . . 16 Itv ;
90 lngndx 23581 . . . . . . . . . . . . . . . 16 LineG ;
9189, 90neeq12i 2756 . . . . . . . . . . . . . . 15 Itv LineG ; ;
9288, 91mpbir 209 . . . . . . . . . . . . . 14 Itv LineG
9379, 92setsnid 14531 . . . . . . . . . . . . 13 Itv sSet Itv Itv sSet Itv sSet LineG
9478, 93syl6eqr 2526 . . . . . . . . . . . 12 Itv Itv sSet Itv
95 ttgval.i . . . . . . . . . . . . 13 Itv
9695a1i 11 . . . . . . . . . . . 12 Itv
9779setsid 14530 . . . . . . . . . . . . 13 Itv sSet Itv
9838, 97mpdan 668 . . . . . . . . . . . 12 Itv sSet Itv
9994, 96, 983eqtr4d 2518 . . . . . . . . . . 11
10099oveqd 6300 . . . . . . . . . 10
101100eleq2d 2537 . . . . . . . . 9
10299oveqd 6300 . . . . . . . . . 10
103102eleq2d 2537 . . . . . . . . 9
10499oveqd 6300 . . . . . . . . . 10
105104eleq2d 2537 . . . . . . . . 9
106101, 103, 1053orbi123d 1298 . . . . . . . 8
107106rabbidv 3105 . . . . . . 7
1081073ad2ant1 1017 . . . . . 6
109108mpt2eq3dva 6344 . . . . 5
110109opeq2d 4220 . . . 4 LineG LineG
111110oveq2d 6299 . . 3 sSet Itv sSet LineG sSet Itv sSet LineG
11277, 111eqtr4d 2511 . 2 sSet Itv sSet LineG
113112, 99jca 532 1 sSet Itv sSet LineG
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   w3o 972   wceq 1379   wcel 1767   wne 2662  wrex 2815  crab 2818  cvv 3113  csb 3435  cop 4033  cfv 5587  (class class class)co 6283   cmpt2 6285  cc0 9491  c1 9492  c6 10588  c7 10589  ;cdc 10975  cicc 11531  cnx 14486   sSet csts 14487  cbs 14489  cvsca 14558  csg 15729  Itvcitv 23576  LineGclng 23577  toTGcttg 23868 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-cnex 9547  ax-resscn 9548  ax-1cn 9549  ax-icn 9550  ax-addcl 9551  ax-addrcl 9552  ax-mulcl 9553  ax-mulrcl 9554  ax-mulcom 9555  ax-addass 9556  ax-mulass 9557  ax-distr 9558  ax-i2m1 9559  ax-1ne0 9560  ax-1rid 9561  ax-rnegex 9562  ax-rrecex 9563  ax-cnre 9564  ax-pre-lttri 9565  ax-pre-lttrn 9566  ax-pre-ltadd 9567  ax-pre-mulgt0 9568 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-riota 6244  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-om 6680  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-er 7311  df-en 7517  df-dom 7518  df-sdom 7519  df-pnf 9629  df-mnf 9630  df-xr 9631  df-ltxr 9632  df-le 9633  df-sub 9806  df-neg 9807  df-nn 10536  df-2 10593  df-3 10594  df-4 10595  df-5 10596  df-6 10597  df-7 10598  df-8 10599  df-9 10600  df-10 10601  df-n0 10795  df-dec 10976  df-ndx 14492  df-slot 14493  df-sets 14495  df-itv 23578  df-lng 23579  df-ttg 23869 This theorem is referenced by:  ttglem  23871  ttgitvval  23877
 Copyright terms: Public domain W3C validator