isperp

Description: Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019)

	Ref	Expression
Hypotheses	isperp.p	$⊢ P = {Base}_{G}$
	isperp.d	$⊢ \underset{˙}{-} = dist (G)$
	isperp.i	$⊢ I = Itv (G)$
	isperp.l	$⊢ L = {Line}_{𝒢} (G)$
	isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isperp.a	$⊢ φ \to A \in ran L$
	isperp.b	$⊢ φ \to B \in ran L$
Assertion	isperp	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$⊢ P = {Base}_{G}$
2		isperp.d	$⊢ \underset{˙}{-} = dist (G)$
3		isperp.i	$⊢ I = Itv (G)$
4		isperp.l	$⊢ L = {Line}_{𝒢} (G)$
5		isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		isperp.a	$⊢ φ \to A \in ran L$
7		isperp.b	$⊢ φ \to B \in ran L$
8		df-br	$⊢ A ⟂_{𝒢} (G) B \leftrightarrow ⟨A, B⟩ \in ⟂_{𝒢} (G)$
9		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))\})$
10		simpr	$⊢ (φ \land g = G) \to g = G$
11	10	fveq2d	$⊢ (φ \land g = G) \to {Line}_{𝒢} (g) = {Line}_{𝒢} (G)$
12	11 4	eqtr4di	$⊢ (φ \land g = G) \to {Line}_{𝒢} (g) = L$
13	12	rneqd	$⊢ (φ \land g = G) \to ran {Line}_{𝒢} (g) = ran L$
14	13	eleq2d	$⊢ (φ \land g = G) \to (a \in ran {Line}_{𝒢} (g) \leftrightarrow a \in ran L)$
15	13	eleq2d	$⊢ (φ \land g = G) \to (b \in ran {Line}_{𝒢} (g) \leftrightarrow b \in ran L)$
16	14 15	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))$
17	10	fveq2d	$⊢ (φ \land g = G) \to ∟_{𝒢} (g) = ∟_{𝒢} (G)$
18	17	eleq2d	$⊢ (φ \land g = G) \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (g) \leftrightarrow ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
19	18	ralbidv	$⊢ (φ \land g = G) \to (\forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (g) \leftrightarrow \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
20	19	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))$
21	16 20	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)))$
22	21	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))\}$
23	5	elexd	$⊢ φ \to G \in V$
24	4	fvexi	$⊢ L \in V$
25		rnexg	$⊢ L \in V \to ran L \in V$
26	24 25	mp1i	$⊢ φ \to ran L \in V$
27	26 26	xpexd	$⊢ φ \to ran L \times ran L \in V$
28		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$
29	28	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$
30	27 29	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$
31	9 22 23 30	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))\}$
32	31	eleq2d	$⊢ φ \to (⟨A, B⟩ \in ⟂_{𝒢} (G) \leftrightarrow ⟨A, B⟩ \in \{⟨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	8 32	bitrid	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow ⟨A, B⟩ \in \{⟨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		ineq12	$⊢ (a = A \land b = B) \to a \cap b = A \cap B$
35		simpll	$⊢ ((a = A \land b = B) \land x \in (a \cap b)) \to a = A$
36		simpllr	$⊢ (((a = A \land b = B) \land x \in (a \cap b)) \land u \in a) \to b = B$
37	36	raleqdv	$⊢ (((a = A \land b = B) \land x \in (a \cap b)) \land u \in a) \to (\forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
38	35 37	raleqbidva	$⊢ ((a = A \land b = B) \land x \in (a \cap b)) \to (\forall u \in a \forall v \in b ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
39	34 38	rexeqbidva	$⊢ (a = A \land b = B) \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))$
40	39	opelopab2a	$⊢ (A \in ran L \land B \in ran L) \to (⟨A, B⟩ \in \{⟨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))\} \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
41	6 7 40	syl2anc	$⊢ φ \to (⟨A, B⟩ \in \{⟨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))\} \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
42	33 41	bitrd	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$

Metamath Proof Explorer

Theorem isperp

Proof