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	eqcomd	$⊢ (p = P \land i = I) \to P = p$
13	12	difeq1d	$⊢ (p = P \land i = I) \to P ∖ d = p ∖ d$
14	13	eleq2d	$⊢ (p = P \land i = I) \to (a \in (P ∖ d) \leftrightarrow a \in (p ∖ d))$
15	13	eleq2d	$⊢ (p = P \land i = I) \to (c \in (P ∖ d) \leftrightarrow c \in (p ∖ d))$
16	14 15	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)))$
17		simpr	$⊢ (p = P \land i = I) \to i = I$
18	17	eqcomd	$⊢ (p = P \land i = I) \to I = i$
19	18	oveqd	$⊢ (p = P \land i = I) \to a I c = a i c$
20	19	eleq2d	$⊢ (p = P \land i = I) \to (t \in (a I c) \leftrightarrow t \in (a i c))$
21	20	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))$
22	16 21	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)))$
23	13	eleq2d	$⊢ (p = P \land i = I) \to (b \in (P ∖ d) \leftrightarrow b \in (p ∖ d))$
24	23 15	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)))$
25	18	oveqd	$⊢ (p = P \land i = I) \to b I c = b i c$
26	25	eleq2d	$⊢ (p = P \land i = I) \to (t \in (b I c) \leftrightarrow t \in (b i c))$
27	26	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))$
28	24 27	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)))$
29	22 28	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))))$
30	12 29	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))))$
31	1 2 30	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))))$
32	31	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)))\}$
33	10 32	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)))\})$
34		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)))\}))$
35	3	fvexi	$⊢ L \in V$
36	35	rnex	$⊢ ran L \in V$
37	36	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$
38	33 34 37	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)))\})$
39	5 7 38	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)))\})$
40		difeq2	$⊢ d = D \to P ∖ d = P ∖ D$
41	40	eleq2d	$⊢ d = D \to (a \in (P ∖ d) \leftrightarrow a \in (P ∖ D))$
42	40	eleq2d	$⊢ d = D \to (c \in (P ∖ d) \leftrightarrow c \in (P ∖ D))$
43	41 42	anbi12d	$⊢ d = D \to ((a \in (P ∖ d) \land c \in (P ∖ d)) \leftrightarrow (a \in (P ∖ D) \land c \in (P ∖ D)))$
44		rexeq	$⊢ d = D \to (\exists t \in d t \in (a I c) \leftrightarrow \exists t \in D t \in (a I c))$
45	43 44	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)))$
46	40	eleq2d	$⊢ d = D \to (b \in (P ∖ d) \leftrightarrow b \in (P ∖ D))$
47	46 42	anbi12d	$⊢ d = D \to ((b \in (P ∖ d) \land c \in (P ∖ d)) \leftrightarrow (b \in (P ∖ D) \land c \in (P ∖ D)))$
48		rexeq	$⊢ d = D \to (\exists t \in d t \in (b I c) \leftrightarrow \exists t \in D t \in (b I c))$
49	47 48	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)))$
50	45 49	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))))$
51	50	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))))$
52	51	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)))\}$
53	52	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)))\}$
54		df-xp	$⊢ P \times P = \{⟨a, b⟩ \| (a \in P \land b \in P)\}$
55	1	fvexi	$⊢ P \in V$
56	55 55	xpex	$⊢ P \times P \in V$
57	54 56	eqeltrri	$⊢ \{⟨a, b⟩ \| (a \in P \land b \in P)\} \in V$
58		eldifi	$⊢ a \in (P ∖ D) \to a \in P$
59		eldifi	$⊢ b \in (P ∖ D) \to b \in P$
60	58 59	anim12i	$⊢ (a \in (P ∖ D) \land b \in (P ∖ D)) \to (a \in P \land b \in P)$
61	60	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)$
62	61	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)$
63	62	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)$
64	63	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)\}$
65	57 64	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$
66	65	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$
67	39 53 6 66	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)))\}$
68		vex	$⊢ a \in V$
69		vex	$⊢ c \in V$
70		eleq1w	$⊢ e = a \to (e \in (P ∖ D) \leftrightarrow a \in (P ∖ D))$
71	70	anbi1d	$⊢ e = a \to ((e \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (a \in (P ∖ D) \land f \in (P ∖ D)))$
72		oveq1	$⊢ e = a \to e I f = a I f$
73	72	eleq2d	$⊢ e = a \to (t \in (e I f) \leftrightarrow t \in (a I f))$
74	73	rexbidv	$⊢ e = a \to (\exists t \in D t \in (e I f) \leftrightarrow \exists t \in D t \in (a I f))$
75	71 74	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)))$
76		eleq1w	$⊢ f = c \to (f \in (P ∖ D) \leftrightarrow c \in (P ∖ D))$
77	76	anbi2d	$⊢ f = c \to ((a \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (a \in (P ∖ D) \land c \in (P ∖ D)))$
78		oveq2	$⊢ f = c \to a I f = a I c$
79	78	eleq2d	$⊢ f = c \to (t \in (a I f) \leftrightarrow t \in (a I c))$
80	79	rexbidv	$⊢ f = c \to (\exists t \in D t \in (a I f) \leftrightarrow \exists t \in D t \in (a I c))$
81	77 80	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)))$
82		simpl	$⊢ (a = e \land b = f) \to a = e$
83	82	eleq1d	$⊢ (a = e \land b = f) \to (a \in (P ∖ D) \leftrightarrow e \in (P ∖ D))$
84		simpr	$⊢ (a = e \land b = f) \to b = f$
85	84	eleq1d	$⊢ (a = e \land b = f) \to (b \in (P ∖ D) \leftrightarrow f \in (P ∖ D))$
86	83 85	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)))$
87		oveq12	$⊢ (a = e \land b = f) \to a I b = e I f$
88	87	eleq2d	$⊢ (a = e \land b = f) \to (t \in (a I b) \leftrightarrow t \in (e I f))$
89	88	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))$
90	86 89	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)))$
91	90	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))\}$
92	4 91	eqtri	$⊢ O = \{⟨e, f⟩ \| ((e \in (P ∖ D) \land f \in (P ∖ D)) \land \exists t \in D t \in (e I f))\}$
93	68 69 75 81 92	brab	$⊢ a O c \leftrightarrow ((a \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (a I c))$
94		vex	$⊢ b \in V$
95		eleq1w	$⊢ e = b \to (e \in (P ∖ D) \leftrightarrow b \in (P ∖ D))$
96	95	anbi1d	$⊢ e = b \to ((e \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (b \in (P ∖ D) \land f \in (P ∖ D)))$
97		oveq1	$⊢ e = b \to e I f = b I f$
98	97	eleq2d	$⊢ e = b \to (t \in (e I f) \leftrightarrow t \in (b I f))$
99	98	rexbidv	$⊢ e = b \to (\exists t \in D t \in (e I f) \leftrightarrow \exists t \in D t \in (b I f))$
100	96 99	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)))$
101	76	anbi2d	$⊢ f = c \to ((b \in (P ∖ D) \land f \in (P ∖ D)) \leftrightarrow (b \in (P ∖ D) \land c \in (P ∖ D)))$
102		oveq2	$⊢ f = c \to b I f = b I c$
103	102	eleq2d	$⊢ f = c \to (t \in (b I f) \leftrightarrow t \in (b I c))$
104	103	rexbidv	$⊢ f = c \to (\exists t \in D t \in (b I f) \leftrightarrow \exists t \in D t \in (b I c))$
105	101 104	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)))$
106	94 69 100 105 92	brab	$⊢ b O c \leftrightarrow ((b \in (P ∖ D) \land c \in (P ∖ D)) \land \exists t \in D t \in (b I c))$
107	93 106	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)))$
108	107	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)))$
109	108	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)))\}$
110	67 109	eqtr4di	$⊢ φ \to {hp}_{𝒢} (G) (D) = \{⟨a, b⟩ \| \exists c \in P (a O c \land b O c)\}$

Metamath Proof Explorer

Theorem ishpg

Proof