MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ttglem Structured version   Visualization version   GIF version

Theorem ttglem 26345
Description: Lemma for ttgbas 26346 and ttgvsca 26349. (Contributed by Thierry Arnoux, 15-Apr-2019.)
Hypotheses
Ref Expression
ttgval.n 𝐺 = (toTG‘𝐻)
ttglem.2 𝐸 = Slot 𝑁
ttglem.3 𝑁 ∈ ℕ
ttglem.4 𝑁 < 16
Assertion
Ref Expression
ttglem (𝐸𝐻) = (𝐸𝐺)

Proof of Theorem ttglem
Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ttgval.n . . . . . 6 𝐺 = (toTG‘𝐻)
2 eqid 2795 . . . . . 6 (Base‘𝐻) = (Base‘𝐻)
3 eqid 2795 . . . . . 6 (-g𝐻) = (-g𝐻)
4 eqid 2795 . . . . . 6 ( ·𝑠𝐻) = ( ·𝑠𝐻)
5 eqid 2795 . . . . . 6 (Itv‘𝐺) = (Itv‘𝐺)
61, 2, 3, 4, 5ttgval 26344 . . . . 5 (𝐻 ∈ V → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})⟩) ∧ (Itv‘𝐺) = (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})))
76simpld 495 . . . 4 (𝐻 ∈ V → 𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})⟩))
87fveq2d 6542 . . 3 (𝐻 ∈ V → (𝐸𝐺) = (𝐸‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})⟩)))
9 ttglem.2 . . . . . 6 𝐸 = Slot 𝑁
10 ttglem.3 . . . . . 6 𝑁 ∈ ℕ
119, 10ndxid 16338 . . . . 5 𝐸 = Slot (𝐸‘ndx)
1210nnrei 11495 . . . . . . 7 𝑁 ∈ ℝ
13 ttglem.4 . . . . . . 7 𝑁 < 16
1412, 13ltneii 10600 . . . . . 6 𝑁16
159, 10ndxarg 16337 . . . . . . 7 (𝐸‘ndx) = 𝑁
16 itvndx 25908 . . . . . . 7 (Itv‘ndx) = 16
1715, 16neeq12i 3050 . . . . . 6 ((𝐸‘ndx) ≠ (Itv‘ndx) ↔ 𝑁16)
1814, 17mpbir 232 . . . . 5 (𝐸‘ndx) ≠ (Itv‘ndx)
1911, 18setsnid 16368 . . . 4 (𝐸𝐻) = (𝐸‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩))
20 1nn0 11761 . . . . . . . . 9 1 ∈ ℕ0
21 6nn0 11766 . . . . . . . . 9 6 ∈ ℕ0
22 7nn 11577 . . . . . . . . 9 7 ∈ ℕ
23 6lt7 11671 . . . . . . . . 9 6 < 7
2420, 21, 22, 23declt 11975 . . . . . . . 8 16 < 17
25 6nn 11574 . . . . . . . . . . 11 6 ∈ ℕ
2620, 25decnncl 11967 . . . . . . . . . 10 16 ∈ ℕ
2726nnrei 11495 . . . . . . . . 9 16 ∈ ℝ
2820, 22decnncl 11967 . . . . . . . . . 10 17 ∈ ℕ
2928nnrei 11495 . . . . . . . . 9 17 ∈ ℝ
3012, 27, 29lttri 10613 . . . . . . . 8 ((𝑁 < 16 ∧ 16 < 17) → 𝑁 < 17)
3113, 24, 30mp2an 688 . . . . . . 7 𝑁 < 17
3212, 31ltneii 10600 . . . . . 6 𝑁17
33 lngndx 25909 . . . . . . 7 (LineG‘ndx) = 17
3415, 33neeq12i 3050 . . . . . 6 ((𝐸‘ndx) ≠ (LineG‘ndx) ↔ 𝑁17)
3532, 34mpbir 232 . . . . 5 (𝐸‘ndx) ≠ (LineG‘ndx)
3611, 35setsnid 16368 . . . 4 (𝐸‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩)) = (𝐸‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})⟩))
3719, 36eqtri 2819 . . 3 (𝐸𝐻) = (𝐸‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝐻)𝑥) = (𝑘( ·𝑠𝐻)(𝑦(-g𝐻)𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})⟩))
388, 37syl6reqr 2850 . 2 (𝐻 ∈ V → (𝐸𝐻) = (𝐸𝐺))
399str0 16364 . . 3 ∅ = (𝐸‘∅)
40 fvprc 6531 . . 3 𝐻 ∈ V → (𝐸𝐻) = ∅)
41 fvprc 6531 . . . . 5 𝐻 ∈ V → (toTG‘𝐻) = ∅)
421, 41syl5eq 2843 . . . 4 𝐻 ∈ V → 𝐺 = ∅)
4342fveq2d 6542 . . 3 𝐻 ∈ V → (𝐸𝐺) = (𝐸‘∅))
4439, 40, 433eqtr4a 2857 . 2 𝐻 ∈ V → (𝐸𝐻) = (𝐸𝐺))
4538, 44pm2.61i 183 1 (𝐸𝐻) = (𝐸𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  w3o 1079   = wceq 1522  wcel 2081  wne 2984  wrex 3106  {crab 3109  Vcvv 3437  c0 4211  cop 4478   class class class wbr 4962  cfv 6225  (class class class)co 7016  cmpo 7018  0cc0 10383  1c1 10384   < clt 10521  cn 11486  6c6 11544  7c7 11545  cdc 11947  [,]cicc 12591  ndxcnx 16309   sSet csts 16310  Slot cslot 16311  Basecbs 16312   ·𝑠 cvsca 16398  -gcsg 17863  Itvcitv 25904  LineGclng 25905  toTGcttg 26342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5081  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-fal 1535  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-2 11548  df-3 11549  df-4 11550  df-5 11551  df-6 11552  df-7 11553  df-8 11554  df-9 11555  df-n0 11746  df-dec 11948  df-ndx 16315  df-slot 16316  df-sets 16319  df-itv 25906  df-lng 25907  df-ttg 26343
This theorem is referenced by:  ttgbas  26346  ttgplusg  26347  ttgvsca  26349  ttgds  26350
  Copyright terms: Public domain W3C validator