perpln2

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	perpln2	$⊢ φ \to B \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	syl6eqr	$⊢ (φ \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	26	rneqd	$⊢ φ \to ran ⟂_{𝒢} (G) = ran \{⟨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))\}$
28	23	rnssi	$⊢ ran \{⟨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 (ran L \times ran L)$
29	27 28	eqsstrdi	$⊢ φ \to ran ⟂_{𝒢} (G) \subseteq ran (ran L \times ran L)$
30		rnxpss	$⊢ ran (ran L \times ran L) \subseteq ran L$
31	29 30	sstrdi	$⊢ φ \to ran ⟂_{𝒢} (G) \subseteq ran L$
32		relopab	$⊢ 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))\}$
33	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))\})$
34	32 33	mpbiri	$⊢ φ \to Rel ⟂_{𝒢} (G)$
35		brrelex12	$⊢ (Rel ⟂_{𝒢} (G) \land A ⟂_{𝒢} (G) B) \to (A \in V \land B \in V)$
36	34 3 35	syl2anc	$⊢ φ \to (A \in V \land B \in V)$
37	36	simpld	$⊢ φ \to A \in V$
38	36	simprd	$⊢ φ \to B \in V$
39		brelrng	$⊢ (A \in V \land B \in V \land A ⟂_{𝒢} (G) B) \to B \in ran ⟂_{𝒢} (G)$
40	37 38 3 39	syl3anc	$⊢ φ \to B \in ran ⟂_{𝒢} (G)$
41	31 40	sseldd	$⊢ φ \to B \in ran L$

Metamath Proof Explorer

Theorem perpln2

Proof