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

Theorem ishlg 26074
Description: Rays : Definition 6.1 of [Schwabhauser] p. 43. With this definition, 𝐴(𝐾𝐶)𝐵 means that 𝐴 and 𝐵 are on the same ray with initial point 𝐶. This follows the same notation as Schwabhauser where rays are first defined as a relation. It is possible to recover the ray itself using e.g. ((𝐾𝐶) “ {𝐴}) (Contributed by Thierry Arnoux, 21-Dec-2019.)
Hypotheses
Ref Expression
ishlg.p 𝑃 = (Base‘𝐺)
ishlg.i 𝐼 = (Itv‘𝐺)
ishlg.k 𝐾 = (hlG‘𝐺)
ishlg.a (𝜑𝐴𝑃)
ishlg.b (𝜑𝐵𝑃)
ishlg.c (𝜑𝐶𝑃)
ishlg.g (𝜑𝐺𝑉)
Assertion
Ref Expression
ishlg (𝜑 → (𝐴(𝐾𝐶)𝐵 ↔ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))

Proof of Theorem ishlg
Dummy variables 𝑎 𝑏 𝑐 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 483 . . . . . 6 ((𝑎 = 𝐴𝑏 = 𝐵) → 𝑎 = 𝐴)
21neeq1d 3045 . . . . 5 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑎𝐶𝐴𝐶))
3 simpr 485 . . . . . 6 ((𝑎 = 𝐴𝑏 = 𝐵) → 𝑏 = 𝐵)
43neeq1d 3045 . . . . 5 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑏𝐶𝐵𝐶))
53oveq2d 7039 . . . . . . 7 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝐶𝐼𝑏) = (𝐶𝐼𝐵))
61, 5eleq12d 2879 . . . . . 6 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑎 ∈ (𝐶𝐼𝑏) ↔ 𝐴 ∈ (𝐶𝐼𝐵)))
71oveq2d 7039 . . . . . . 7 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝐶𝐼𝑎) = (𝐶𝐼𝐴))
83, 7eleq12d 2879 . . . . . 6 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑏 ∈ (𝐶𝐼𝑎) ↔ 𝐵 ∈ (𝐶𝐼𝐴)))
96, 8orbi12d 913 . . . . 5 ((𝑎 = 𝐴𝑏 = 𝐵) → ((𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)) ↔ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))
102, 4, 93anbi123d 1428 . . . 4 ((𝑎 = 𝐴𝑏 = 𝐵) → ((𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))) ↔ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
11 eqid 2797 . . . 4 {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}
1210, 11brab2a 5537 . . 3 (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴𝑃𝐵𝑃) ∧ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
1312a1i 11 . 2 (𝜑 → (𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵 ↔ ((𝐴𝑃𝐵𝑃) ∧ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))))
14 ishlg.k . . . . 5 𝐾 = (hlG‘𝐺)
15 ishlg.g . . . . . 6 (𝜑𝐺𝑉)
16 elex 3458 . . . . . 6 (𝐺𝑉𝐺 ∈ V)
17 fveq2 6545 . . . . . . . . 9 (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺))
18 ishlg.p . . . . . . . . 9 𝑃 = (Base‘𝐺)
1917, 18syl6eqr 2851 . . . . . . . 8 (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃)
2019eleq2d 2870 . . . . . . . . . . 11 (𝑔 = 𝐺 → (𝑎 ∈ (Base‘𝑔) ↔ 𝑎𝑃))
2119eleq2d 2870 . . . . . . . . . . 11 (𝑔 = 𝐺 → (𝑏 ∈ (Base‘𝑔) ↔ 𝑏𝑃))
2220, 21anbi12d 630 . . . . . . . . . 10 (𝑔 = 𝐺 → ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ↔ (𝑎𝑃𝑏𝑃)))
23 fveq2 6545 . . . . . . . . . . . . . . 15 (𝑔 = 𝐺 → (Itv‘𝑔) = (Itv‘𝐺))
24 ishlg.i . . . . . . . . . . . . . . 15 𝐼 = (Itv‘𝐺)
2523, 24syl6eqr 2851 . . . . . . . . . . . . . 14 (𝑔 = 𝐺 → (Itv‘𝑔) = 𝐼)
2625oveqd 7040 . . . . . . . . . . . . 13 (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑏) = (𝑐𝐼𝑏))
2726eleq2d 2870 . . . . . . . . . . . 12 (𝑔 = 𝐺 → (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ↔ 𝑎 ∈ (𝑐𝐼𝑏)))
2825oveqd 7040 . . . . . . . . . . . . 13 (𝑔 = 𝐺 → (𝑐(Itv‘𝑔)𝑎) = (𝑐𝐼𝑎))
2928eleq2d 2870 . . . . . . . . . . . 12 (𝑔 = 𝐺 → (𝑏 ∈ (𝑐(Itv‘𝑔)𝑎) ↔ 𝑏 ∈ (𝑐𝐼𝑎)))
3027, 29orbi12d 913 . . . . . . . . . . 11 (𝑔 = 𝐺 → ((𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)) ↔ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))
31303anbi3d 1434 . . . . . . . . . 10 (𝑔 = 𝐺 → ((𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))) ↔ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))))
3222, 31anbi12d 630 . . . . . . . . 9 (𝑔 = 𝐺 → (((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎)))) ↔ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))))
3332opabbidv 5034 . . . . . . . 8 (𝑔 = 𝐺 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))})
3419, 33mpteq12dv 5052 . . . . . . 7 (𝑔 = 𝐺 → (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}) = (𝑐𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
35 df-hlg 26073 . . . . . . 7 hlG = (𝑔 ∈ V ↦ (𝑐 ∈ (Base‘𝑔) ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑔) ∧ 𝑏 ∈ (Base‘𝑔)) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐(Itv‘𝑔)𝑏) ∨ 𝑏 ∈ (𝑐(Itv‘𝑔)𝑎))))}))
3634, 35, 18mptfvmpt 6863 . . . . . 6 (𝐺 ∈ V → (hlG‘𝐺) = (𝑐𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
3715, 16, 363syl 18 . . . . 5 (𝜑 → (hlG‘𝐺) = (𝑐𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
3814, 37syl5eq 2845 . . . 4 (𝜑𝐾 = (𝑐𝑃 ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))}))
39 neeq2 3049 . . . . . . . 8 (𝑐 = 𝐶 → (𝑎𝑐𝑎𝐶))
40 neeq2 3049 . . . . . . . 8 (𝑐 = 𝐶 → (𝑏𝑐𝑏𝐶))
41 oveq1 7030 . . . . . . . . . 10 (𝑐 = 𝐶 → (𝑐𝐼𝑏) = (𝐶𝐼𝑏))
4241eleq2d 2870 . . . . . . . . 9 (𝑐 = 𝐶 → (𝑎 ∈ (𝑐𝐼𝑏) ↔ 𝑎 ∈ (𝐶𝐼𝑏)))
43 oveq1 7030 . . . . . . . . . 10 (𝑐 = 𝐶 → (𝑐𝐼𝑎) = (𝐶𝐼𝑎))
4443eleq2d 2870 . . . . . . . . 9 (𝑐 = 𝐶 → (𝑏 ∈ (𝑐𝐼𝑎) ↔ 𝑏 ∈ (𝐶𝐼𝑎)))
4542, 44orbi12d 913 . . . . . . . 8 (𝑐 = 𝐶 → ((𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)) ↔ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))
4639, 40, 453anbi123d 1428 . . . . . . 7 (𝑐 = 𝐶 → ((𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))) ↔ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎)))))
4746anbi2d 628 . . . . . 6 (𝑐 = 𝐶 → (((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎)))) ↔ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))))
4847opabbidv 5034 . . . . 5 (𝑐 = 𝐶 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
4948adantl 482 . . . 4 ((𝜑𝑐 = 𝐶) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝑐𝑏𝑐 ∧ (𝑎 ∈ (𝑐𝐼𝑏) ∨ 𝑏 ∈ (𝑐𝐼𝑎))))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
50 ishlg.c . . . 4 (𝜑𝐶𝑃)
5118fvexi 6559 . . . . . . 7 𝑃 ∈ V
5251, 51xpex 7340 . . . . . 6 (𝑃 × 𝑃) ∈ V
53 opabssxp 5536 . . . . . 6 {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ⊆ (𝑃 × 𝑃)
5452, 53ssexi 5124 . . . . 5 {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V
5554a1i 11 . . . 4 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))} ∈ V)
5638, 49, 50, 55fvmptd 6648 . . 3 (𝜑 → (𝐾𝐶) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))})
5756breqd 4979 . 2 (𝜑 → (𝐴(𝐾𝐶)𝐵𝐴{⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑃𝑏𝑃) ∧ (𝑎𝐶𝑏𝐶 ∧ (𝑎 ∈ (𝐶𝐼𝑏) ∨ 𝑏 ∈ (𝐶𝐼𝑎))))}𝐵))
58 ishlg.a . . . 4 (𝜑𝐴𝑃)
59 ishlg.b . . . 4 (𝜑𝐵𝑃)
6058, 59jca 512 . . 3 (𝜑 → (𝐴𝑃𝐵𝑃))
6160biantrurd 533 . 2 (𝜑 → ((𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))) ↔ ((𝐴𝑃𝐵𝑃) ∧ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴))))))
6213, 57, 613bitr4d 312 1 (𝜑 → (𝐴(𝐾𝐶)𝐵 ↔ (𝐴𝐶𝐵𝐶 ∧ (𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐶𝐼𝐴)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wo 842  w3a 1080   = wceq 1525  wcel 2083  wne 2986  Vcvv 3440   class class class wbr 4968  {copab 5030  cmpt 5047   × cxp 5448  cfv 6232  (class class class)co 7023  Basecbs 16316  Itvcitv 25908  hlGchlg 26072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-hlg 26073
This theorem is referenced by:  hlcomb  26075  hlne1  26077  hlne2  26078  hlln  26079  hlid  26081  hltr  26082  hlbtwn  26083  btwnhl1  26084  btwnhl2  26085  btwnhl  26086  lnhl  26087  hlcgrex  26088  mirhl  26151  mirbtwnhl  26152  mirhl2  26153  opphllem4  26222  opphl  26226  hlpasch  26228  lnopp2hpgb  26235  cgracgr  26290  cgraswap  26292  flatcgra  26296  cgrahl  26299  cgracol  26300
  Copyright terms: Public domain W3C validator