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

Theorem ttgval 25668
Description: Define a function to augment a subcomplex Hilbert space with betweenness and a line definition. (Contributed by Thierry Arnoux, 25-Mar-2019.)
Hypotheses
Ref Expression
ttgval.n 𝐺 = (toTG‘𝐻)
ttgval.b 𝐵 = (Base‘𝐻)
ttgval.m = (-g𝐻)
ttgval.s · = ( ·𝑠𝐻)
ttgval.i 𝐼 = (Itv‘𝐺)
Assertion
Ref Expression
ttgval (𝐻𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})))
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 3201 . . . . 5 (𝐻𝑉𝐻 ∈ V)
4 fveq2 6153 . . . . . . . . . 10 (𝑤 = 𝐻 → (Base‘𝑤) = (Base‘𝐻))
5 ttgval.b . . . . . . . . . 10 𝐵 = (Base‘𝐻)
64, 5syl6eqr 2673 . . . . . . . . 9 (𝑤 = 𝐻 → (Base‘𝑤) = 𝐵)
7 fveq2 6153 . . . . . . . . . . . . . 14 (𝑤 = 𝐻 → (-g𝑤) = (-g𝐻))
8 ttgval.m . . . . . . . . . . . . . 14 = (-g𝐻)
97, 8syl6eqr 2673 . . . . . . . . . . . . 13 (𝑤 = 𝐻 → (-g𝑤) = )
109oveqd 6627 . . . . . . . . . . . 12 (𝑤 = 𝐻 → (𝑧(-g𝑤)𝑥) = (𝑧 𝑥))
11 fveq2 6153 . . . . . . . . . . . . . 14 (𝑤 = 𝐻 → ( ·𝑠𝑤) = ( ·𝑠𝐻))
12 ttgval.s . . . . . . . . . . . . . 14 · = ( ·𝑠𝐻)
1311, 12syl6eqr 2673 . . . . . . . . . . . . 13 (𝑤 = 𝐻 → ( ·𝑠𝑤) = · )
14 eqidd 2622 . . . . . . . . . . . . 13 (𝑤 = 𝐻𝑘 = 𝑘)
159oveqd 6627 . . . . . . . . . . . . 13 (𝑤 = 𝐻 → (𝑦(-g𝑤)𝑥) = (𝑦 𝑥))
1613, 14, 15oveq123d 6631 . . . . . . . . . . . 12 (𝑤 = 𝐻 → (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥)) = (𝑘 · (𝑦 𝑥)))
1710, 16eqeq12d 2636 . . . . . . . . . . 11 (𝑤 = 𝐻 → ((𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥)) ↔ (𝑧 𝑥) = (𝑘 · (𝑦 𝑥))))
1817rexbidv 3046 . . . . . . . . . 10 (𝑤 = 𝐻 → (∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))))
196, 18rabeqbidv 3184 . . . . . . . . 9 (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))} = {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})
206, 6, 19mpt2eq123dv 6677 . . . . . . . 8 (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}))
2120csbeq1d 3525 . . . . . . 7 (𝑤 = 𝐻(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
22 oveq1 6617 . . . . . . . . 9 (𝑤 = 𝐻 → (𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩))
23 rabeq 3182 . . . . . . . . . . . 12 ((Base‘𝑤) = 𝐵 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
246, 23syl 17 . . . . . . . . . . 11 (𝑤 = 𝐻 → {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})
256, 6, 24mpt2eq123dv 6677 . . . . . . . . . 10 (𝑤 = 𝐻 → (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}))
2625opeq2d 4382 . . . . . . . . 9 (𝑤 = 𝐻 → ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩)
2722, 26oveq12d 6628 . . . . . . . 8 (𝑤 = 𝐻 → ((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
2827csbeq2dv 3969 . . . . . . 7 (𝑤 = 𝐻(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
2921, 28eqtrd 2655 . . . . . 6 (𝑤 = 𝐻(𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
30 df-ttg 25667 . . . . . 6 toTG = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g𝑤)𝑥) = (𝑘( ·𝑠𝑤)(𝑦(-g𝑤)𝑥))}) / 𝑖((𝑤 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥 ∈ (Base‘𝑤), 𝑦 ∈ (Base‘𝑤) ↦ {𝑧 ∈ (Base‘𝑤) ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
31 ovex 6638 . . . . . . 7 ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
3231csbex 4758 . . . . . 6 (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) ∈ V
3329, 30, 32fvmpt 6244 . . . . 5 (𝐻 ∈ V → (toTG‘𝐻) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
343, 33syl 17 . . . 4 (𝐻𝑉 → (toTG‘𝐻) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩))
35 fvex 6163 . . . . . . . 8 (Base‘𝐻) ∈ V
365, 35eqeltri 2694 . . . . . . 7 𝐵 ∈ V
3736, 36mpt2ex 7199 . . . . . 6 (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) ∈ V
3837a1i 11 . . . . 5 (𝐻𝑉 → (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) ∈ V)
39 simpr 477 . . . . . . 7 ((𝐻𝑉𝑖 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})) → 𝑖 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}))
40 oveq2 6618 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝑐 𝑎) = (𝑐 𝑥))
41 oveq2 6618 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (𝑏 𝑎) = (𝑏 𝑥))
4241oveq2d 6626 . . . . . . . . . . 11 (𝑎 = 𝑥 → (𝑘 · (𝑏 𝑎)) = (𝑘 · (𝑏 𝑥)))
4340, 42eqeq12d 2636 . . . . . . . . . 10 (𝑎 = 𝑥 → ((𝑐 𝑎) = (𝑘 · (𝑏 𝑎)) ↔ (𝑐 𝑥) = (𝑘 · (𝑏 𝑥))))
4443rexbidv 3046 . . . . . . . . 9 (𝑎 = 𝑥 → (∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑏 𝑥))))
4544rabbidv 3180 . . . . . . . 8 (𝑎 = 𝑥 → {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))} = {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑏 𝑥))})
46 oveq1 6617 . . . . . . . . . . . . 13 (𝑏 = 𝑦 → (𝑏 𝑥) = (𝑦 𝑥))
4746oveq2d 6626 . . . . . . . . . . . 12 (𝑏 = 𝑦 → (𝑘 · (𝑏 𝑥)) = (𝑘 · (𝑦 𝑥)))
4847eqeq2d 2631 . . . . . . . . . . 11 (𝑏 = 𝑦 → ((𝑐 𝑥) = (𝑘 · (𝑏 𝑥)) ↔ (𝑐 𝑥) = (𝑘 · (𝑦 𝑥))))
4948rexbidv 3046 . . . . . . . . . 10 (𝑏 = 𝑦 → (∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑏 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑦 𝑥))))
5049rabbidv 3180 . . . . . . . . 9 (𝑏 = 𝑦 → {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑏 𝑥))} = {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑦 𝑥))})
51 oveq1 6617 . . . . . . . . . . . 12 (𝑐 = 𝑧 → (𝑐 𝑥) = (𝑧 𝑥))
5251eqeq1d 2623 . . . . . . . . . . 11 (𝑐 = 𝑧 → ((𝑐 𝑥) = (𝑘 · (𝑦 𝑥)) ↔ (𝑧 𝑥) = (𝑘 · (𝑦 𝑥))))
5352rexbidv 3046 . . . . . . . . . 10 (𝑐 = 𝑧 → (∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑦 𝑥)) ↔ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))))
5453cbvrabv 3188 . . . . . . . . 9 {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑦 𝑥))} = {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}
5550, 54syl6eq 2671 . . . . . . . 8 (𝑏 = 𝑦 → {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑥) = (𝑘 · (𝑏 𝑥))} = {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})
5645, 55cbvmpt2v 6695 . . . . . . 7 (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))}) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})
5739, 56syl6eqr 2673 . . . . . 6 ((𝐻𝑉𝑖 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})) → 𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))}))
58 simpr 477 . . . . . . . . . 10 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → 𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))}))
5958, 56syl6eq 2671 . . . . . . . . 9 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → 𝑖 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}))
6059opeq2d 4382 . . . . . . . 8 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → ⟨(Itv‘ndx), 𝑖⟩ = ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩)
6160oveq2d 6626 . . . . . . 7 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) = (𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩))
6259oveqd 6627 . . . . . . . . . . . 12 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑥𝑖𝑦) = (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦))
6362eleq2d 2684 . . . . . . . . . . 11 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑧 ∈ (𝑥𝑖𝑦) ↔ 𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦)))
6459oveqd 6627 . . . . . . . . . . . 12 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑧𝑖𝑦) = (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦))
6564eleq2d 2684 . . . . . . . . . . 11 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑥 ∈ (𝑧𝑖𝑦) ↔ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦)))
6659oveqd 6627 . . . . . . . . . . . 12 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑥𝑖𝑧) = (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))
6766eleq2d 2684 . . . . . . . . . . 11 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑦 ∈ (𝑥𝑖𝑧) ↔ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧)))
6863, 65, 673orbi123d 1395 . . . . . . . . . 10 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → ((𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))))
6968rabbidv 3180 . . . . . . . . 9 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))} = {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})
7069mpt2eq3dv 6681 . . . . . . . 8 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))}) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))}))
7170opeq2d 4382 . . . . . . 7 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩)
7261, 71oveq12d 6628 . . . . . 6 ((𝐻𝑉𝑖 = (𝑎𝐵, 𝑏𝐵 ↦ {𝑐𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑐 𝑎) = (𝑘 · (𝑏 𝑎))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
7357, 72syldan 487 . . . . 5 ((𝐻𝑉𝑖 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})) → ((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
7438, 73csbied 3545 . . . 4 (𝐻𝑉(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) / 𝑖((𝐻 sSet ⟨(Itv‘ndx), 𝑖⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
752, 34, 743eqtrd 2659 . . 3 (𝐻𝑉𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
7675fveq2d 6157 . . . . . . . . . . . 12 (𝐻𝑉 → (Itv‘𝐺) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩)))
77 itvid 25254 . . . . . . . . . . . . 13 Itv = Slot (Itv‘ndx)
78 1nn0 11259 . . . . . . . . . . . . . . . . 17 1 ∈ ℕ0
79 6nn 11140 . . . . . . . . . . . . . . . . 17 6 ∈ ℕ
8078, 79decnncl 11469 . . . . . . . . . . . . . . . 16 16 ∈ ℕ
8180nnrei 10980 . . . . . . . . . . . . . . 15 16 ∈ ℝ
82 6nn0 11264 . . . . . . . . . . . . . . . 16 6 ∈ ℕ0
83 7nn 11141 . . . . . . . . . . . . . . . 16 7 ∈ ℕ
84 6lt7 11160 . . . . . . . . . . . . . . . 16 6 < 7
8578, 82, 83, 84declt 11481 . . . . . . . . . . . . . . 15 16 < 17
8681, 85ltneii 10101 . . . . . . . . . . . . . 14 16 ≠ 17
87 itvndx 25252 . . . . . . . . . . . . . . 15 (Itv‘ndx) = 16
88 lngndx 25253 . . . . . . . . . . . . . . 15 (LineG‘ndx) = 17
8987, 88neeq12i 2856 . . . . . . . . . . . . . 14 ((Itv‘ndx) ≠ (LineG‘ndx) ↔ 16 ≠ 17)
9086, 89mpbir 221 . . . . . . . . . . . . 13 (Itv‘ndx) ≠ (LineG‘ndx)
9177, 90setsnid 15843 . . . . . . . . . . . 12 (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩)) = (Itv‘((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
9276, 91syl6eqr 2673 . . . . . . . . . . 11 (𝐻𝑉 → (Itv‘𝐺) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩)))
93 ttgval.i . . . . . . . . . . . 12 𝐼 = (Itv‘𝐺)
9493a1i 11 . . . . . . . . . . 11 (𝐻𝑉𝐼 = (Itv‘𝐺))
9577setsid 15842 . . . . . . . . . . . 12 ((𝐻𝑉 ∧ (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) ∈ V) → (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩)))
9637, 95mpan2 706 . . . . . . . . . . 11 (𝐻𝑉 → (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}) = (Itv‘(𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩)))
9792, 94, 963eqtr4d 2665 . . . . . . . . . 10 (𝐻𝑉𝐼 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))}))
9897oveqd 6627 . . . . . . . . 9 (𝐻𝑉 → (𝑥𝐼𝑦) = (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦))
9998eleq2d 2684 . . . . . . . 8 (𝐻𝑉 → (𝑧 ∈ (𝑥𝐼𝑦) ↔ 𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦)))
10097oveqd 6627 . . . . . . . . 9 (𝐻𝑉 → (𝑧𝐼𝑦) = (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦))
101100eleq2d 2684 . . . . . . . 8 (𝐻𝑉 → (𝑥 ∈ (𝑧𝐼𝑦) ↔ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦)))
10297oveqd 6627 . . . . . . . . 9 (𝐻𝑉 → (𝑥𝐼𝑧) = (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))
103102eleq2d 2684 . . . . . . . 8 (𝐻𝑉 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧)))
10499, 101, 1033orbi123d 1395 . . . . . . 7 (𝐻𝑉 → ((𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧)) ↔ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))))
105104rabbidv 3180 . . . . . 6 (𝐻𝑉 → {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} = {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})
106105mpt2eq3dv 6681 . . . . 5 (𝐻𝑉 → (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))}))
107106opeq2d 4382 . . . 4 (𝐻𝑉 → ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩ = ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩)
108107oveq2d 6626 . . 3 (𝐻𝑉 → ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑥 ∈ (𝑧(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑦) ∨ 𝑦 ∈ (𝑥(𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})𝑧))})⟩))
10975, 108eqtr4d 2658 . 2 (𝐻𝑉𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩))
110109, 97jca 554 1 (𝐻𝑉 → (𝐺 = ((𝐻 sSet ⟨(Itv‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})⟩) sSet ⟨(LineG‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})⟩) ∧ 𝐼 = (𝑥𝐵, 𝑦𝐵 ↦ {𝑧𝐵 ∣ ∃𝑘 ∈ (0[,]1)(𝑧 𝑥) = (𝑘 · (𝑦 𝑥))})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3o 1035   = wceq 1480  wcel 1987  wne 2790  wrex 2908  {crab 2911  Vcvv 3189  csb 3518  cop 4159  cfv 5852  (class class class)co 6610  cmpt2 6612  0cc0 9887  1c1 9888  6c6 11025  7c7 11026  cdc 11444  [,]cicc 12127  ndxcnx 15785   sSet csts 15786  Basecbs 15788   ·𝑠 cvsca 15873  -gcsg 17352  Itvcitv 25248  LineGclng 25249  toTGcttg 25666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-dec 11445  df-ndx 15791  df-slot 15792  df-sets 15794  df-itv 25250  df-lng 25251  df-ttg 25667
This theorem is referenced by:  ttglem  25669  ttgitvval  25675
  Copyright terms: Public domain W3C validator