perpln1

Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019)

	Ref	Expression
Hypotheses	perpln.l	$⊢ L = {Line}_{𝒢} (G)$
	perpln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
	perpln.2	$⊢ φ \to A ⟂_{𝒢} (G) B$
Assertion	perpln1	$⊢ φ \to A \in ran L$

Proof

Step	Hyp	Ref	Expression
1		perpln.l	$⊢ L = {Line}_{𝒢} (G)$
2		perpln.1	$⊢ φ \to G \in 𝒢_{Tarski}$
3		perpln.2	$⊢ φ \to A ⟂_{𝒢} (G) B$
4		df-perpg	$⊢ ⟂_{𝒢} = (g \in V ⟼ \{⟨a, b⟩ \| ((a \in ran {Line}_{𝒢} (g) \land b \in ran {Line}_{𝒢} (g)) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g))\})$
5		simpr	$⊢ (φ \land g = G) \to g = G$
6	5	fveq2d	$⊢ (φ \land g = G) \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
7	6 1	eqtr4di	$⊢ (φ \land g = G) \to {Line}_{𝒢} (g) = L$
8	7	rneqd	$⊢ (φ \land g = G) \to ran {Line}_{𝒢} (g) = ran L$
9	8	eleq2d	$⊢ (φ \land g = G) \to (a \in ran {Line}_{𝒢} (g) \leftrightarrow a \in ran L)$
10	8	eleq2d	$⊢ (φ \land g = G) \to (b \in ran {Line}_{𝒢} (g) \leftrightarrow b \in ran L)$
11	9 10	anbi12d	$⊢ (φ \land g = G) \to ((a \in ran {Line}_{𝒢} (g) \land b \in ran {Line}_{𝒢} (g)) \leftrightarrow (a \in ran L \land b \in ran L))$
12	5	fveq2d	$⊢ (φ \land g = G) \to ∟_{𝒢} (g) = ∟_{𝒢} (G)$
13	12	eleq2d	$⊢ (φ \land g = G) \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (g) \leftrightarrow ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
14	13	ralbidv	$⊢ (φ \land g = G) \to (\forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g) \leftrightarrow \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
15	14	rexralbidv	$⊢ (φ \land g = G) \to (\exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g) \leftrightarrow \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
16	11 15	anbi12d	$⊢ (φ \land g = G) \to (((a \in ran {Line}_{𝒢} (g) \land b \in ran {Line}_{𝒢} (g)) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g)) \leftrightarrow ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))$
17	16	opabbidv	$⊢ (φ \land g = G) \to \{⟨a, b⟩ \| ((a \in ran {Line}_{𝒢} (g) \land b \in ran {Line}_{𝒢} (g)) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g))\} = \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\}$
18	2	elexd	$⊢ φ \to G \in V$
19	1	fvexi	$⊢ L \in V$
20		rnexg	$⊢ L \in V \to ran L \in V$
21	19 20	mp1i	$⊢ φ \to ran L \in V$
22	21 21	xpexd	$⊢ φ \to ran L \times ran L \in V$
23		opabssxp	$⊢ \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\} \subseteq ran L \times ran L$
24	23	a1i	$⊢ φ \to \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\} \subseteq ran L \times ran L$
25	22 24	ssexd	$⊢ φ \to \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\} \in V$
26	4 17 18 25	fvmptd2	$⊢ φ \to ⟂_{𝒢} (G) = \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\}$
27		anass	$⊢ ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \leftrightarrow (a \in ran L \land (b \in ran L \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))$
28	27	opabbii	$⊢ \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\} = \{⟨a, b⟩ \| (a \in ran L \land (b \in ran L \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))\}$
29	26 28	eqtrdi	$⊢ φ \to ⟂_{𝒢} (G) = \{⟨a, b⟩ \| (a \in ran L \land (b \in ran L \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))\}$
30	29	dmeqd	$⊢ φ \to dom ⟂_{𝒢} (G) = dom \{⟨a, b⟩ \| (a \in ran L \land (b \in ran L \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))\}$
31		dmopabss	$⊢ dom \{⟨a, b⟩ \| (a \in ran L \land (b \in ran L \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)))\} \subseteq ran L$
32	30 31	eqsstrdi	$⊢ φ \to dom ⟂_{𝒢} (G) \subseteq ran L$
33		relopabv	$⊢ Rel \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\}$
34	26	releqd	$⊢ φ \to (Rel ⟂_{𝒢} (G) \leftrightarrow Rel \{⟨a, b⟩ \| ((a \in ran L \land b \in ran L) \land \exists x \in (a \cap b) \forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))\})$
35	33 34	mpbiri	$⊢ φ \to Rel ⟂_{𝒢} (G)$
36		brrelex12	$⊢ (Rel ⟂_{𝒢} (G) \land A ⟂_{𝒢} (G) B) \to (A \in V \land B \in V)$
37	35 3 36	syl2anc	$⊢ φ \to (A \in V \land B \in V)$
38	37	simpld	$⊢ φ \to A \in V$
39	37	simprd	$⊢ φ \to B \in V$
40		breldmg	$⊢ (A \in V \land B \in V \land A ⟂_{𝒢} (G) B) \to A \in dom ⟂_{𝒢} (G)$
41	38 39 3 40	syl3anc	$⊢ φ \to A \in dom ⟂_{𝒢} (G)$
42	32 41	sseldd	$⊢ φ \to A \in ran L$

Metamath Proof Explorer

Theorem perpln1

Proof