Metamath Proof Explorer

Theorem ishlg

Description: Rays : Definition 6.1 of Schwabhauser p. 43. With this definition, A ( KC ) B means that A and B are on the same ray with initial point C . 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., ( ( KC ) " { A } ) . (Contributed by Thierry Arnoux, 21-Dec-2019)

Ref Expression
Hypotheses ishlg.p ⊢ P = Base G
ishlg.i ⊢ I = Itv ⁡ G
ishlg.k ⊢ K = hl 𝒢 ⁡ G
ishlg.a ⊢ φ → A ∈ P
ishlg.b ⊢ φ → B ∈ P
ishlg.c ⊢ φ → C ∈ P
ishlg.g ⊢ φ → G ∈ V
Assertion ishlg ⊢ φ → A K ⁡ C B ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A

Proof

Step Hyp Ref Expression
1 ishlg.p ⊢ P = Base G
2 ishlg.i ⊢ I = Itv ⁡ G
3 ishlg.k ⊢ K = hl 𝒢 ⁡ G
4 ishlg.a ⊢ φ → A ∈ P
5 ishlg.b ⊢ φ → B ∈ P
6 ishlg.c ⊢ φ → C ∈ P
7 ishlg.g ⊢ φ → G ∈ V
8 simpl ⊢ a = A ∧ b = B → a = A
9 8 neeq1d ⊢ a = A ∧ b = B → a ≠ C ↔ A ≠ C
10 simpr ⊢ a = A ∧ b = B → b = B
11 10 neeq1d ⊢ a = A ∧ b = B → b ≠ C ↔ B ≠ C
12 10 oveq2d ⊢ a = A ∧ b = B → C I b = C I B
13 8 12 eleq12d ⊢ a = A ∧ b = B → a ∈ C I b ↔ A ∈ C I B
14 8 oveq2d ⊢ a = A ∧ b = B → C I a = C I A
15 10 14 eleq12d ⊢ a = A ∧ b = B → b ∈ C I a ↔ B ∈ C I A
16 13 15 orbi12d ⊢ a = A ∧ b = B → a ∈ C I b ∨ b ∈ C I a ↔ A ∈ C I B ∨ B ∈ C I A
17 9 11 16 3anbi123d ⊢ a = A ∧ b = B → a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
18 eqid ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
19 17 18 brab2a ⊢ A a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a B ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
20 19 a1i ⊢ φ → A a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a B ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
21 elex ⊢ G ∈ V → G ∈ V
22 fveq2 ⊢ g = G → Base g = Base G
23 22 1 eqtr4di ⊢ g = G → Base g = P
24 23 eleq2d ⊢ g = G → a ∈ Base g ↔ a ∈ P
25 23 eleq2d ⊢ g = G → b ∈ Base g ↔ b ∈ P
26 24 25 anbi12d ⊢ g = G → a ∈ Base g ∧ b ∈ Base g ↔ a ∈ P ∧ b ∈ P
27 fveq2 ⊢ g = G → Itv ⁡ g = Itv ⁡ G
28 27 2 eqtr4di ⊢ g = G → Itv ⁡ g = I
29 28 oveqd ⊢ g = G → c Itv ⁡ g b = c I b
30 29 eleq2d ⊢ g = G → a ∈ c Itv ⁡ g b ↔ a ∈ c I b
31 28 oveqd ⊢ g = G → c Itv ⁡ g a = c I a
32 31 eleq2d ⊢ g = G → b ∈ c Itv ⁡ g a ↔ b ∈ c I a
33 30 32 orbi12d ⊢ g = G → a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ∈ c I b ∨ b ∈ c I a
34 33 3anbi3d ⊢ g = G → a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
35 26 34 anbi12d ⊢ g = G → a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a ↔ a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
36 35 opabbidv ⊢ g = G → a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
37 23 36 mpteq12dv ⊢ g = G → c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
38 df-hlg ⊢ hl 𝒢 = g ∈ V ⟼ c ∈ Base g ⟼ a b | a ∈ Base g ∧ b ∈ Base g ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c Itv ⁡ g b ∨ b ∈ c Itv ⁡ g a
39 37 38 1 mptfvmpt ⊢ G ∈ V → hl 𝒢 ⁡ G = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
40 7 21 39 3syl ⊢ φ → hl 𝒢 ⁡ G = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
41 3 40 syl5eq ⊢ φ → K = c ∈ P ⟼ a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a
42 neeq2 ⊢ c = C → a ≠ c ↔ a ≠ C
43 neeq2 ⊢ c = C → b ≠ c ↔ b ≠ C
44 oveq1 ⊢ c = C → c I b = C I b
45 44 eleq2d ⊢ c = C → a ∈ c I b ↔ a ∈ C I b
46 oveq1 ⊢ c = C → c I a = C I a
47 46 eleq2d ⊢ c = C → b ∈ c I a ↔ b ∈ C I a
48 45 47 orbi12d ⊢ c = C → a ∈ c I b ∨ b ∈ c I a ↔ a ∈ C I b ∨ b ∈ C I a
49 42 43 48 3anbi123d ⊢ c = C → a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a ↔ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
50 49 anbi2d ⊢ c = C → a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a ↔ a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
51 50 opabbidv ⊢ c = C → a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
52 51 adantl ⊢ φ ∧ c = C → a b | a ∈ P ∧ b ∈ P ∧ a ≠ c ∧ b ≠ c ∧ a ∈ c I b ∨ b ∈ c I a = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
53 1 fvexi ⊢ P ∈ V
54 53 53 xpex ⊢ P × P ∈ V
55 opabssxp ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ⊆ P × P
56 54 55 ssexi ⊢ a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ∈ V
57 56 a1i ⊢ φ → a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a ∈ V
58 41 52 6 57 fvmptd ⊢ φ → K ⁡ C = a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a
59 58 breqd ⊢ φ → A K ⁡ C B ↔ A a b | a ∈ P ∧ b ∈ P ∧ a ≠ C ∧ b ≠ C ∧ a ∈ C I b ∨ b ∈ C I a B
60 4 5 jca ⊢ φ → A ∈ P ∧ B ∈ P
61 60 biantrurd ⊢ φ → A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A ↔ A ∈ P ∧ B ∈ P ∧ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A
62 20 59 61 3bitr4d ⊢ φ → A K ⁡ C B ↔ A ≠ C ∧ B ≠ C ∧ A ∈ C I B ∨ B ∈ C I A