perpdrag

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019)

	Ref	Expression
Hypotheses	colperpex.p	$⊢ P = {Base}_{G}$
	colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
	colperpex.i	$⊢ I = Itv (G)$
	colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
	colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	perpdrag.1	$⊢ φ \to A \in D$
	perpdrag.2	$⊢ φ \to B \in D$
	perpdrag.3	$⊢ φ \to C \in P$
	perpdrag.4	$⊢ φ \to D ⟂_{𝒢} (G) (B L C)$
Assertion	perpdrag	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	$⊢ P = {Base}_{G}$
2		colperpex.d	$⊢ \underset{˙}{-} = dist (G)$
3		colperpex.i	$⊢ I = Itv (G)$
4		colperpex.l	$⊢ L = {Line}_{𝒢} (G)$
5		colperpex.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		perpdrag.1	$⊢ φ \to A \in D$
7		perpdrag.2	$⊢ φ \to B \in D$
8		perpdrag.3	$⊢ φ \to C \in P$
9		perpdrag.4	$⊢ φ \to D ⟂_{𝒢} (G) (B L C)$
10	5	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to G \in 𝒢_{Tarski}$
11	9	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to D ⟂_{𝒢} (G) (B L C)$
12	4 10 11	perpln1	$⊢ ((φ \land x \in D) \land A \neq x) \to D \in ran L$
13	6	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to A \in D$
14	1 4 3 10 12 13	tglnpt	$⊢ ((φ \land x \in D) \land A \neq x) \to A \in P$
15		simplr	$⊢ ((φ \land x \in D) \land A \neq x) \to x \in D$
16	1 4 3 10 12 15	tglnpt	$⊢ ((φ \land x \in D) \land A \neq x) \to x \in P$
17	7	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to B \in D$
18		simpr	$⊢ ((φ \land x \in D) \land A \neq x) \to A \neq x$
19	1 3 4 10 14 16 18 18 12 13 15	tglinethru	$⊢ ((φ \land x \in D) \land A \neq x) \to D = A L x$
20	17 19	eleqtrd	$⊢ ((φ \land x \in D) \land A \neq x) \to B \in (A L x)$
21	8	ad2antrr	$⊢ ((φ \land x \in D) \land A \neq x) \to C \in P$
22	19 11	eqbrtrrd	$⊢ ((φ \land x \in D) \land A \neq x) \to (A L x) ⟂_{𝒢} (G) (B L C)$
23	1 2 3 4 10 14 16 20 21 22	perprag	$⊢ ((φ \land x \in D) \land A \neq x) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
24	4 5 9	perpln1	$⊢ φ \to D \in ran L$
25	1 3 4 5 24 6	tglnpt2	$⊢ φ \to \exists x \in D A \neq x$
26	23 25	r19.29a	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem perpdrag

Proof