isperp2

Description: Property for 2 lines A, B, intersecting at a point X to be perpendicular. Item (i) of definition 8.13 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$
	isperp2.b	$⊢ φ \to B \in ran L$
	isperp2.x	$⊢ φ \to X \in (A \cap B)$
Assertion	isperp2	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \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		isperp2.b	$⊢ φ \to B \in ran L$
8		isperp2.x	$⊢ φ \to X \in (A \cap B)$
9		eqidd	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to u = u$
10	5	ad4antr	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to G \in 𝒢_{Tarski}$
11	6	ad4antr	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to A \in ran L$
12	7	ad4antr	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to B \in ran L$
13		simp-4r	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to A ⟂_{𝒢} (G) B$
14	1 2 3 4 10 11 12 13	perpneq	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to A \neq B$
15		simpllr	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to x \in (A \cap B)$
16	8	ad4antr	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to X \in (A \cap B)$
17	1 3 4 10 11 12 14 15 16	tglineineq	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to x = X$
18		eqidd	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to v = v$
19	9 17 18	s3eqd	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to ⟨“ u x v ”⟩ = ⟨“ u X v ”⟩$
20	19	eleq1d	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
21	20	biimpd	$⊢ ((((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \land v \in B) \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \to ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
22	21	ralimdva	$⊢ (((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land u \in A) \to (\forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \to \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
23	22	ralimdva	$⊢ ((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \to (\forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \to \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
24	23	imp	$⊢ (((φ \land A ⟂_{𝒢} (G) B) \land x \in (A \cap B)) \land \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)) \to \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)$
25	1 2 3 4 5 6 7	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))$
26	25	biimpa	$⊢ (φ \land A ⟂_{𝒢} (G) B) \to \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
27	24 26	r19.29a	$⊢ (φ \land A ⟂_{𝒢} (G) B) \to \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)$
28		s3eq2	$⊢ x = X \to ⟨“ u x v ”⟩ = ⟨“ u X v ”⟩$
29	28	eleq1d	$⊢ x = X \to (⟨“ u x v ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$
30	29	2ralbidv	$⊢ x = X \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))$
31	30	rspcev	$⊢ (X \in (A \cap B) \land \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)) \to \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
32	8 31	sylan	$⊢ (φ \land \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)) \to \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G)$
33	25	adantr	$⊢ (φ \land \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)) \to (A ⟂_{𝒢} (G) B \leftrightarrow \exists x \in (A \cap B) \forall u \in A \forall v \in B ⟨“ u x v ”⟩ \in ∟_{𝒢} (G))$
34	32 33	mpbird	$⊢ (φ \land \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G)) \to A ⟂_{𝒢} (G) B$
35	27 34	impbida	$⊢ φ \to (A ⟂_{𝒢} (G) B \leftrightarrow \forall u \in A \forall v \in B ⟨“ u X v ”⟩ \in ∟_{𝒢} (G))$

Metamath Proof Explorer

Theorem isperp2

Proof