ishpg

Description: Value of the half-plane relation for a given line D . (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	ishpg.p	$⊢ P = {Base}_{G}$
	ishpg.i	$⊢ I = Itv (G)$
	ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
	ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ishpg.d	$⊢ φ \to D \in ran L$
Assertion	ishpg	$⊢ φ \to {hp}_{𝒢} (G) (D) = \{⟨a, b⟩ \| \exists c \in P (a O c \land b O c)\}$

Proof

Step	Hyp	Ref	Expression
1		ishpg.p	$⊢ P = {Base}_{G}$
2		ishpg.i	$⊢ I = Itv (G)$
3		ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
4		ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		ishpg.d	$⊢ φ \to D \in ran L$
7		elex	$⊢ G \in 𝒢_{Tarski} \to G \in V$
8		fveq2	$⊢ g = G \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
9	8 3	eqtr4di	$⊢ g = G \to {Line}_{𝒢} (g) = L$
10	9	rneqd	$⊢ g = G \to ran {Line}_{𝒢} (g) = ran L$
11		simpl	$⊢ (p = P \land i = I) \to p = P$
12	11	difeq1d	$⊢ (p = P \land i = I) \to p ∖ d = P ∖ d$
13	12	eleq2d	$⊢ (p = P \land i = I) \to (a \in (p ∖ d) \leftrightarrow a \in (P ∖ d))$
14	12	eleq2d	$⊢ (p = P \land i = I) \to (c \in (p ∖ d) \leftrightarrow c \in (P ∖ d))$
15	13 14	anbi12d	$⊢ (p = P \land i = I) \to ((a \in (p ∖ d) \land c \in (p ∖ d)) \leftrightarrow (a \in (P ∖ d) \land c \in (P ∖ d)))$
16		simpr	$⊢ (p = P \land i = I) \to i = I$
17	16	oveqd	$⊢ (p = P \land i = I) \to a i c = a I c$
18	17	eleq2d	$⊢ (p = P \land i = I) \to (t \in (a i c) \leftrightarrow t \in (a I c))$
19	18	rexbidv	$⊢ (p = P \land i = I) \to (\exists t \in d t \in (a i c) \leftrightarrow \exists t \in d t \in (a I c))$
20	15 19	anbi12d	$⊢ (p = P \land i = I) \to (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \leftrightarrow ((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)))$
21	12	eleq2d	$⊢ (p = P \land i = I) \to (b \in (p ∖ d) \leftrightarrow b \in (P ∖ d))$
22	21 14	anbi12d	$⊢ (p = P \land i = I) \to ((b \in (p ∖ d) \land c \in (p ∖ d)) \leftrightarrow (b \in (P ∖ d) \land c \in (P ∖ d)))$
23	16	oveqd	$⊢ (p = P \land i = I) \to b i c = b I c$
24	23	eleq2d	$⊢ (p = P \land i = I) \to (t \in (b i c) \leftrightarrow t \in (b I c))$
25	24	rexbidv	$⊢ (p = P \land i = I) \to (\exists t \in d t \in (b i c) \leftrightarrow \exists t \in d t \in (b I c))$
26	22 25	anbi12d	$⊢ (p = P \land i = I) \to (((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c)) \leftrightarrow ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))$
27	20 26	anbi12d	$⊢ (p = P \land i = I) \to ((((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c))) \leftrightarrow (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c))))$
28	11 27	rexeqbidv	$⊢ (p = P \land i = I) \to (\exists c \in p (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c))) \leftrightarrow \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c))))$
29	1 2 28	sbcie2s	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists c \in p (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c))) \leftrightarrow \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c))))$
30	29	opabbidv	$⊢ g = G \to \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists c \in p (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c)))\} = \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\}$
31	10 30	mpteq12dv	$⊢ g = G \to (d \in ran {Line}_{𝒢} (g) ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists c \in p (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c)))\}) = (d \in ran L ⟼ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\})$
32		df-hpg	$⊢ {hp}_{𝒢} = (g \in V ⟼ (d \in ran {Line}_{𝒢} (g) ⟼ \{⟨a, b⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists c \in p (((a \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (a i c)) \land ((b \in (p ∖ d) \land c \in (p ∖ d)) \land \exists t \in d t \in (b i c)))\}))$
33	3	fvexi	$⊢ L \in V$
34	33	rnex	$⊢ ran L \in V$
35	34	mptex	$⊢ (d \in ran L ⟼ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\}) \in V$
36	31 32 35	fvmpt	$⊢ G \in V \to {hp}_{𝒢} (G) = (d \in ran L ⟼ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\})$
37	5 7 36	3syl	$⊢ φ \to {hp}_{𝒢} (G) = (d \in ran L ⟼ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\})$
38		difeq2	$⊢ d = D \to P ∖ d = P ∖ D$
39	38	eleq2d	$⊢ d = D \to (a \in (P ∖ d) \leftrightarrow a \in (P ∖ D))$
40	38	eleq2d	$⊢ d = D \to (c \in (P ∖ d) \leftrightarrow c \in (P ∖ D))$
41	39 40	anbi12d	$⊢ d = D \to ((a \in (P ∖ d) \land c \in (P ∖ d)) \leftrightarrow (a \in (P ∖ D) \land c \in (P ∖ D)))$
42		rexeq	$⊢ d = D \to (\exists t \in d t \in (a I c) \leftrightarrow \exists t \in D t \in (a I c))$
43	41 42	anbi12d	$⊢ d = D \to (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \leftrightarrow ((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)))$
44	38	eleq2d	$⊢ d = D \to (b \in (P ∖ d) \leftrightarrow b \in (P ∖ D))$
45	44 40	anbi12d	$⊢ d = D \to ((b \in (P ∖ d) \land c \in (P ∖ d)) \leftrightarrow (b \in (P ∖ D) \land c \in (P ∖ D)))$
46		rexeq	$⊢ d = D \to (\exists t \in d t \in (b I c) \leftrightarrow \exists t \in D t \in (b I c))$
47	45 46	anbi12d	$⊢ d = D \to (((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)) \leftrightarrow ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))$
48	43 47	anbi12d	$⊢ d = D \to ((((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c))) \leftrightarrow (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))))$
49	48	rexbidv	$⊢ d = D \to (\exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c))) \leftrightarrow \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))))$
50	49	opabbidv	$⊢ d = D \to \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\} = \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\}$
51	50	adantl	$⊢ (φ \land d = D) \to \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (a I c)) \land ((b \in (P ∖ d) \land c \in (P ∖ d)) \land \exists t \in d t \in (b I c)))\} = \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\}$
52		df-xp	$⊢ P \times P = \{⟨a, b⟩ \| (a \in P \land b \in P)\}$
53	1	fvexi	$⊢ P \in V$
54	53 53	xpex	$⊢ P \times P \in V$
55	52 54	eqeltrri	$⊢ \{⟨a, b⟩ \| (a \in P \land b \in P)\} \in V$
56		eldifi	$⊢ a \in (P ∖ D) \to a \in P$
57		eldifi	$⊢ b \in (P ∖ D) \to b \in P$
58	56 57	anim12i	$⊢ (a \in (P ∖ D) \land b \in (P ∖ D)) \to (a \in P \land b \in P)$
59	58	ad2ant2r	$⊢ ((a \in (P ∖ D) \land c \in (P ∖ D)) \land (b \in (P ∖ D) \land c \in (P ∖ D))) \to (a \in P \land b \in P)$
60	59	ad2ant2r	$⊢ (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))) \to (a \in P \land b \in P)$
61	60	rexlimivw	$⊢ \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))) \to (a \in P \land b \in P)$
62	61	ssopab2i	$⊢ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\} \subseteq \{⟨a, b⟩ \| (a \in P \land b \in P)\}$
63	55 62	ssexi	$⊢ \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\} \in V$
64	63	a1i	$⊢ φ \to \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\} \in V$
65	37 51 6 64	fvmptd	$⊢ φ \to {hp}_{𝒢} (G) (D) = \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\}$
66		vex	$⊢ a \in V$
67		vex	$⊢ c \in V$
68		eleq1w	$⊢ e = a \to (e \in (P ∖ D) \leftrightarrow a \in (P ∖ D))$
69	68	anbi1d	$⊢ e = a \to ((e \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (a \in (P ∖ D) \land f \in (P ∖ D)))$
70		oveq1	$⊢ e = a \to e I f = a I f$
71	70	eleq2d	$⊢ e = a \to (t \in (e I f) \leftrightarrow t \in (a I f))$
72	71	rexbidv	$⊢ e = a \to (\exists t \in D t \in (e I f) \leftrightarrow \exists t \in D t \in (a I f))$
73	69 72	anbi12d	$⊢ e = a \to (((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f)) \leftrightarrow ((a \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (a I f)))$
74		eleq1w	$⊢ f = c \to (f \in (P ∖ D) \leftrightarrow c \in (P ∖ D))$
75	74	anbi2d	$⊢ f = c \to ((a \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (a \in (P ∖ D) \land c \in (P ∖ D)))$
76		oveq2	$⊢ f = c \to a I f = a I c$
77	76	eleq2d	$⊢ f = c \to (t \in (a I f) \leftrightarrow t \in (a I c))$
78	77	rexbidv	$⊢ f = c \to (\exists t \in D t \in (a I f) \leftrightarrow \exists t \in D t \in (a I c))$
79	75 78	anbi12d	$⊢ f = c \to (((a \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (a I f)) \leftrightarrow ((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)))$
80		simpl	$⊢ (a = e \land b = f) \to a = e$
81	80	eleq1d	$⊢ (a = e \land b = f) \to (a \in (P ∖ D) \leftrightarrow e \in (P ∖ D))$
82		simpr	$⊢ (a = e \land b = f) \to b = f$
83	82	eleq1d	$⊢ (a = e \land b = f) \to (b \in (P ∖ D) \leftrightarrow f \in (P ∖ D))$
84	81 83	anbi12d	$⊢ (a = e \land b = f) \to ((a \in (P ∖ D) \land b \in (P ∖ D)) \leftrightarrow (e \in (P ∖ D) \land f \in (P ∖ D)))$
85		oveq12	$⊢ (a = e \land b = f) \to a I b = e I f$
86	85	eleq2d	$⊢ (a = e \land b = f) \to (t \in (a I b) \leftrightarrow t \in (e I f))$
87	86	rexbidv	$⊢ (a = e \land b = f) \to (\exists t \in D t \in (a I b) \leftrightarrow \exists t \in D t \in (e I f))$
88	84 87	anbi12d	$⊢ (a = e \land b = f) \to (((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b)) \leftrightarrow ((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f)))$
89	88	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\} = \{⟨e, f⟩ \| ((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f))\}$
90	4 89	eqtri	$⊢ O = \{⟨e, f⟩ \| ((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f))\}$
91	66 67 73 79 90	brab	$⊢ a O c \leftrightarrow ((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c))$
92		vex	$⊢ b \in V$
93		eleq1w	$⊢ e = b \to (e \in (P ∖ D) \leftrightarrow b \in (P ∖ D))$
94	93	anbi1d	$⊢ e = b \to ((e \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (b \in (P ∖ D) \land f \in (P ∖ D)))$
95		oveq1	$⊢ e = b \to e I f = b I f$
96	95	eleq2d	$⊢ e = b \to (t \in (e I f) \leftrightarrow t \in (b I f))$
97	96	rexbidv	$⊢ e = b \to (\exists t \in D t \in (e I f) \leftrightarrow \exists t \in D t \in (b I f))$
98	94 97	anbi12d	$⊢ e = b \to (((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f)) \leftrightarrow ((b \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (b I f)))$
99	74	anbi2d	$⊢ f = c \to ((b \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (b \in (P ∖ D) \land c \in (P ∖ D)))$
100		oveq2	$⊢ f = c \to b I f = b I c$
101	100	eleq2d	$⊢ f = c \to (t \in (b I f) \leftrightarrow t \in (b I c))$
102	101	rexbidv	$⊢ f = c \to (\exists t \in D t \in (b I f) \leftrightarrow \exists t \in D t \in (b I c))$
103	99 102	anbi12d	$⊢ f = c \to (((b \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (b I f)) \leftrightarrow ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))$
104	92 67 98 103 90	brab	$⊢ b O c \leftrightarrow ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))$
105	91 104	anbi12i	$⊢ (a O c \land b O c) \leftrightarrow (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))$
106	105	rexbii	$⊢ \exists c \in P (a O c \land b O c) \leftrightarrow \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))$
107	106	opabbii	$⊢ \{⟨a, b⟩ \| \exists c \in P (a O c \land b O c)\} = \{⟨a, b⟩ \| \exists c \in P (((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c)) \land ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c)))\}$
108	65 107	eqtr4di	$⊢ φ \to {hp}_{𝒢} (G) (D) = \{⟨a, b⟩ \| \exists c \in P (a O c \land b O c)\}$

Metamath Proof Explorer

Theorem ishpg

Proof