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

Theorem ttgval 24904
 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 3089 . . . . 5
4 fveq2 5882 . . . . . . . . . 10
5 ttgval.b . . . . . . . . . 10
64, 5syl6eqr 2481 . . . . . . . . 9
7 fveq2 5882 . . . . . . . . . . . . . 14
8 ttgval.m . . . . . . . . . . . . . 14
97, 8syl6eqr 2481 . . . . . . . . . . . . 13
109oveqd 6323 . . . . . . . . . . . 12
11 fveq2 5882 . . . . . . . . . . . . . 14
12 ttgval.s . . . . . . . . . . . . . 14
1311, 12syl6eqr 2481 . . . . . . . . . . . . 13
14 eqidd 2423 . . . . . . . . . . . . 13
159oveqd 6323 . . . . . . . . . . . . 13
1613, 14, 15oveq123d 6327 . . . . . . . . . . . 12
1710, 16eqeq12d 2444 . . . . . . . . . . 11
1817rexbidv 2936 . . . . . . . . . 10
196, 18rabeqbidv 3075 . . . . . . . . 9
206, 6, 19mpt2eq123dv 6368 . . . . . . . 8
2120csbeq1d 3402 . . . . . . 7 sSet Itv sSet LineG sSet Itv sSet LineG
22 oveq1 6313 . . . . . . . . 9 sSet Itv sSet Itv
23 rabeq 3073 . . . . . . . . . . . 12
246, 23syl 17 . . . . . . . . . . 11
256, 6, 24mpt2eq123dv 6368 . . . . . . . . . 10
2625opeq2d 4194 . . . . . . . . 9 LineG LineG
2722, 26oveq12d 6324 . . . . . . . 8 sSet Itv sSet LineG sSet Itv sSet LineG
2827csbeq2dv 3811 . . . . . . 7 sSet Itv sSet LineG sSet Itv sSet LineG
2921, 28eqtrd 2463 . . . . . 6 sSet Itv sSet LineG sSet Itv sSet LineG
30 df-ttg 24903 . . . . . 6 toTG sSet Itv sSet LineG
31 ovex 6334 . . . . . . 7 sSet Itv sSet LineG
3231csbex 4559 . . . . . 6 sSet Itv sSet LineG
3329, 30, 32fvmpt 5965 . . . . 5 toTG sSet Itv sSet LineG
343, 33syl 17 . . . 4 toTG sSet Itv sSet LineG
35 fvex 5892 . . . . . . . 8
365, 35eqeltri 2503 . . . . . . 7
3736, 36mpt2ex 6885 . . . . . 6
3837a1i 11 . . . . 5
39 simpr 462 . . . . . . 7
40 oveq2 6314 . . . . . . . . . . 11
41 oveq2 6314 . . . . . . . . . . . 12
4241oveq2d 6322 . . . . . . . . . . 11
4340, 42eqeq12d 2444 . . . . . . . . . 10
4443rexbidv 2936 . . . . . . . . 9
4544rabbidv 3071 . . . . . . . 8
46 oveq1 6313 . . . . . . . . . . . . 13
4746oveq2d 6322 . . . . . . . . . . . 12
4847eqeq2d 2436 . . . . . . . . . . 11
4948rexbidv 2936 . . . . . . . . . 10
5049rabbidv 3071 . . . . . . . . 9
51 oveq1 6313 . . . . . . . . . . . 12
5251eqeq1d 2424 . . . . . . . . . . 11
5352rexbidv 2936 . . . . . . . . . 10
5453cbvrabv 3079 . . . . . . . . 9
5550, 54syl6eq 2479 . . . . . . . 8
5645, 55cbvmpt2v 6386 . . . . . . 7
5739, 56syl6eqr 2481 . . . . . 6
58 simpr 462 . . . . . . . . . 10
5958, 56syl6eq 2479 . . . . . . . . 9
6059opeq2d 4194 . . . . . . . 8 Itv Itv
6160oveq2d 6322 . . . . . . 7 sSet Itv sSet Itv
6259oveqd 6323 . . . . . . . . . . . 12
6362eleq2d 2492 . . . . . . . . . . 11
6459oveqd 6323 . . . . . . . . . . . 12
6564eleq2d 2492 . . . . . . . . . . 11
6659oveqd 6323 . . . . . . . . . . . 12
6766eleq2d 2492 . . . . . . . . . . 11
6863, 65, 673orbi123d 1334 . . . . . . . . . 10
6968rabbidv 3071 . . . . . . . . 9
7069mpt2eq3dv 6372 . . . . . . . 8
7170opeq2d 4194 . . . . . . 7 LineG LineG
7261, 71oveq12d 6324 . . . . . 6 sSet Itv sSet LineG sSet Itv sSet LineG
7357, 72syldan 472 . . . . 5 sSet Itv sSet LineG sSet Itv sSet LineG
7438, 73csbied 3422 . . . 4 sSet Itv sSet LineG sSet Itv sSet LineG
752, 34, 743eqtrd 2467 . . 3 sSet Itv sSet LineG
7675fveq2d 5886 . . . . . . . . . . . 12 Itv Itv sSet Itv sSet LineG
77 itvid 24489 . . . . . . . . . . . . 13 Itv Slot Itv
78 1nn0 10893 . . . . . . . . . . . . . . . . 17
79 6nn 10779 . . . . . . . . . . . . . . . . 17
8078, 79decnncl 11072 . . . . . . . . . . . . . . . 16 ;
8180nnrei 10626 . . . . . . . . . . . . . . 15 ;
82 6nn0 10898 . . . . . . . . . . . . . . . 16
83 7nn 10780 . . . . . . . . . . . . . . . 16
84 6lt7 10799 . . . . . . . . . . . . . . . 16
8578, 82, 83, 84declt 11080 . . . . . . . . . . . . . . 15 ; ;
8681, 85ltneii 9755 . . . . . . . . . . . . . 14 ; ;
87 itvndx 24487 . . . . . . . . . . . . . . 15 Itv ;
88 lngndx 24488 . . . . . . . . . . . . . . 15 LineG ;
8987, 88neeq12i 2709 . . . . . . . . . . . . . 14 Itv LineG ; ;
9086, 89mpbir 212 . . . . . . . . . . . . 13 Itv LineG
9177, 90setsnid 15165 . . . . . . . . . . . 12 Itv sSet Itv Itv sSet Itv sSet LineG
9276, 91syl6eqr 2481 . . . . . . . . . . 11 Itv Itv sSet Itv
93 ttgval.i . . . . . . . . . . . 12 Itv
9493a1i 11 . . . . . . . . . . 11 Itv
9577setsid 15164 . . . . . . . . . . . 12 Itv sSet Itv
9637, 95mpan2 675 . . . . . . . . . . 11 Itv sSet Itv
9792, 94, 963eqtr4d 2473 . . . . . . . . . 10
9897oveqd 6323 . . . . . . . . 9
9998eleq2d 2492 . . . . . . . 8
10097oveqd 6323 . . . . . . . . 9
101100eleq2d 2492 . . . . . . . 8
10297oveqd 6323 . . . . . . . . 9
103102eleq2d 2492 . . . . . . . 8
10499, 101, 1033orbi123d 1334 . . . . . . 7
105104rabbidv 3071 . . . . . 6
106105mpt2eq3dv 6372 . . . . 5
107106opeq2d 4194 . . . 4 LineG LineG
108107oveq2d 6322 . . 3 sSet Itv sSet LineG sSet Itv sSet LineG
10975, 108eqtr4d 2466 . 2 sSet Itv sSet LineG
110109, 97jca 534 1 sSet Itv sSet LineG
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3o 981   wceq 1437   wcel 1872   wne 2614  wrex 2772  crab 2775  cvv 3080  csb 3395  cop 4004  cfv 5601  (class class class)co 6306   cmpt2 6308  cc0 9547  c1 9548  c6 10671  c7 10672  ;cdc 11059  cicc 11646  cnx 15118   sSet csts 15119  cbs 15121  cvsca 15194  csg 16671  Itvcitv 24483  LineGclng 24484  toTGcttg 24902 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-2 10676  df-3 10677  df-4 10678  df-5 10679  df-6 10680  df-7 10681  df-8 10682  df-9 10683  df-10 10684  df-n0 10878  df-dec 11060  df-ndx 15124  df-slot 15125  df-sets 15127  df-itv 24485  df-lng 24486  df-ttg 24903 This theorem is referenced by:  ttglem  24905  ttgitvval  24911
 Copyright terms: Public domain W3C validator