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	$⊢ φ \to A \in P$
	ishlg.b	$⊢ φ \to B \in P$
	ishlg.c	$⊢ φ \to C \in P$
	ishlg.g	$⊢ φ \to G \in V$
Assertion	ishlg	$⊢ φ \to (A K (C) B \leftrightarrow (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (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	$⊢ φ \to A \in P$
5		ishlg.b	$⊢ φ \to B \in P$
6		ishlg.c	$⊢ φ \to C \in P$
7		ishlg.g	$⊢ φ \to G \in V$
8		simpl	$⊢ (a = A \land b = B) \to a = A$
9	8	neeq1d	$⊢ (a = A \land b = B) \to (a \neq C \leftrightarrow A \neq C)$
10		simpr	$⊢ (a = A \land b = B) \to b = B$
11	10	neeq1d	$⊢ (a = A \land b = B) \to (b \neq C \leftrightarrow B \neq C)$
12	10	oveq2d	$⊢ (a = A \land b = B) \to C I b = C I B$
13	8 12	eleq12d	$⊢ (a = A \land b = B) \to (a \in (C I b) \leftrightarrow A \in (C I B))$
14	8	oveq2d	$⊢ (a = A \land b = B) \to C I a = C I A$
15	10 14	eleq12d	$⊢ (a = A \land b = B) \to (b \in (C I a) \leftrightarrow B \in (C I A))$
16	13 15	orbi12d	$⊢ (a = A \land b = B) \to ((a \in (C I b) \lor b \in (C I a)) \leftrightarrow (A \in (C I B) \lor B \in (C I A)))$
17	9 11 16	3anbi123d	$⊢ (a = A \land b = B) \to ((a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))) \leftrightarrow (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))))$
18		eqid	$⊢ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} = \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\}$
19	17 18	brab2a	$⊢ A \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} B \leftrightarrow ((A \in P \land B \in P) \land (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))))$
20	19	a1i	$⊢ φ \to (A \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} B \leftrightarrow ((A \in P \land B \in P) \land (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A)))))$
21		elex	$⊢ G \in V \to G \in V$
22		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
23	22 1	eqtr4di	$⊢ g = G \to {Base}_{g} = P$
24	23	eleq2d	$⊢ g = G \to (a \in {Base}_{g} \leftrightarrow a \in P)$
25	23	eleq2d	$⊢ g = G \to (b \in {Base}_{g} \leftrightarrow b \in P)$
26	24 25	anbi12d	$⊢ g = G \to ((a \in {Base}_{g} \land b \in {Base}_{g}) \leftrightarrow (a \in P \land b \in P))$
27		fveq2	$⊢ g = G \to Itv (g) = Itv (G)$
28	27 2	eqtr4di	$⊢ g = G \to Itv (g) = I$
29	28	oveqd	$⊢ g = G \to c Itv (g) b = c I b$
30	29	eleq2d	$⊢ g = G \to (a \in (c Itv (g) b) \leftrightarrow a \in (c I b))$
31	28	oveqd	$⊢ g = G \to c Itv (g) a = c I a$
32	31	eleq2d	$⊢ g = G \to (b \in (c Itv (g) a) \leftrightarrow b \in (c I a))$
33	30 32	orbi12d	$⊢ g = G \to ((a \in (c Itv (g) b) \lor b \in (c Itv (g) a)) \leftrightarrow (a \in (c I b) \lor b \in (c I a)))$
34	33	3anbi3d	$⊢ g = G \to ((a \neq c \land b \neq c \land (a \in (c Itv (g) b) \lor b \in (c Itv (g) a))) \leftrightarrow (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))$
35	26 34	anbi12d	$⊢ g = G \to (((a \in {Base}_{g} \land b \in {Base}_{g}) \land (a \neq c \land b \neq c \land (a \in (c Itv (g) b) \lor b \in (c Itv (g) a)))) \leftrightarrow ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a)))))$
36	35	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| ((a \in {Base}_{g} \land b \in {Base}_{g}) \land (a \neq c \land b \neq c \land (a \in (c Itv (g) b) \lor b \in (c Itv (g) a))))\} = \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\}$
37	23 36	mpteq12dv	$⊢ g = G \to (c \in {Base}_{g} ⟼ \{⟨a, b⟩ \| ((a \in {Base}_{g} \land b \in {Base}_{g}) \land (a \neq c \land b \neq c \land (a \in (c Itv (g) b) \lor b \in (c Itv (g) a))))\}) = (c \in P ⟼ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\})$
38		df-hlg	$⊢ {hl}_{𝒢} = (g \in V ⟼ (c \in {Base}_{g} ⟼ \{⟨a, b⟩ \| ((a \in {Base}_{g} \land b \in {Base}_{g}) \land (a \neq c \land b \neq c \land (a \in (c Itv (g) b) \lor b \in (c Itv (g) a))))\}))$
39	37 38 1	mptfvmpt	$⊢ G \in V \to {hl}_{𝒢} (G) = (c \in P ⟼ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\})$
40	7 21 39	3syl	$⊢ φ \to {hl}_{𝒢} (G) = (c \in P ⟼ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\})$
41	3 40	eqtrid	$⊢ φ \to K = (c \in P ⟼ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\})$
42		neeq2	$⊢ c = C \to (a \neq c \leftrightarrow a \neq C)$
43		neeq2	$⊢ c = C \to (b \neq c \leftrightarrow b \neq C)$
44		oveq1	$⊢ c = C \to c I b = C I b$
45	44	eleq2d	$⊢ c = C \to (a \in (c I b) \leftrightarrow a \in (C I b))$
46		oveq1	$⊢ c = C \to c I a = C I a$
47	46	eleq2d	$⊢ c = C \to (b \in (c I a) \leftrightarrow b \in (C I a))$
48	45 47	orbi12d	$⊢ c = C \to ((a \in (c I b) \lor b \in (c I a)) \leftrightarrow (a \in (C I b) \lor b \in (C I a)))$
49	42 43 48	3anbi123d	$⊢ c = C \to ((a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))) \leftrightarrow (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))$
50	49	anbi2d	$⊢ c = C \to (((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a)))) \leftrightarrow ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a)))))$
51	50	opabbidv	$⊢ c = C \to \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\} = \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\}$
52	51	adantl	$⊢ (φ \land c = C) \to \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq c \land b \neq c \land (a \in (c I b) \lor b \in (c I a))))\} = \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\}$
53	1	fvexi	$⊢ P \in V$
54	53 53	xpex	$⊢ P \times P \in V$
55		opabssxp	$⊢ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} \subseteq P \times P$
56	54 55	ssexi	$⊢ \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} \in V$
57	56	a1i	$⊢ φ \to \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} \in V$
58	41 52 6 57	fvmptd	$⊢ φ \to K (C) = \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\}$
59	58	breqd	$⊢ φ \to (A K (C) B \leftrightarrow A \{⟨a, b⟩ \| ((a \in P \land b \in P) \land (a \neq C \land b \neq C \land (a \in (C I b) \lor b \in (C I a))))\} B)$
60	4 5	jca	$⊢ φ \to (A \in P \land B \in P)$
61	60	biantrurd	$⊢ φ \to ((A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))) \leftrightarrow ((A \in P \land B \in P) \land (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A)))))$
62	20 59 61	3bitr4d	$⊢ φ \to (A K (C) B \leftrightarrow (A \neq C \land B \neq C \land (A \in (C I B) \lor B \in (C I A))))$

Metamath Proof Explorer

Theorem ishlg

Proof