perpdragALT

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 12-Dec-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	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	perpdragALT	$⊢ φ \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		eqidd	$⊢ (φ \land A = B) \to A = A$
11		simpr	$⊢ (φ \land A = B) \to A = B$
12		eqidd	$⊢ (φ \land A = B) \to C = C$
13	10 11 12	s3eqd	$⊢ (φ \land A = B) \to ⟨“ A A C ”⟩ = ⟨“ A B C ”⟩$
14		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
15	4 5 9	perpln1	$⊢ φ \to D \in ran L$
16	1 4 3 5 15 6	tglnpt	$⊢ φ \to A \in P$
17	1 2 3 4 14 5 8 16 8	ragtrivb	$⊢ φ \to ⟨“ C A A ”⟩ \in ∟_{𝒢} (G)$
18	1 2 3 4 14 5 8 16 16 17	ragcom	$⊢ φ \to ⟨“ A A C ”⟩ \in ∟_{𝒢} (G)$
19	18	adantr	$⊢ (φ \land A = B) \to ⟨“ A A C ”⟩ \in ∟_{𝒢} (G)$
20	13 19	eqeltrrd	$⊢ (φ \land A = B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
21	5	adantr	$⊢ (φ \land A \neq B) \to G \in 𝒢_{Tarski}$
22	16	adantr	$⊢ (φ \land A \neq B) \to A \in P$
23	1 4 3 5 15 7	tglnpt	$⊢ φ \to B \in P$
24	23	adantr	$⊢ (φ \land A \neq B) \to B \in P$
25	7	adantr	$⊢ (φ \land A \neq B) \to B \in D$
26		simpr	$⊢ (φ \land A \neq B) \to A \neq B$
27	15	adantr	$⊢ (φ \land A \neq B) \to D \in ran L$
28	6	adantr	$⊢ (φ \land A \neq B) \to A \in D$
29	1 3 4 21 22 24 26 26 27 28 25	tglinethru	$⊢ (φ \land A \neq B) \to D = A L B$
30	25 29	eleqtrd	$⊢ (φ \land A \neq B) \to B \in (A L B)$
31	8	adantr	$⊢ (φ \land A \neq B) \to C \in P$
32	9	adantr	$⊢ (φ \land A \neq B) \to D ⟂_{𝒢} (G) (B L C)$
33	29 32	eqbrtrrd	$⊢ (φ \land A \neq B) \to (A L B) ⟂_{𝒢} (G) (B L C)$
34	1 2 3 4 21 22 24 30 31 33	perprag	$⊢ (φ \land A \neq B) \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$
35	20 34	pm2.61dane	$⊢ φ \to ⟨“ A B C ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem perpdragALT

Proof