perprag

Description: Deduce a right angle from perpendicular lines. (Contributed by Thierry Arnoux, 10-Nov-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}$
	perprag.1	$⊢ φ \to A \in P$
	perprag.2	$⊢ φ \to B \in P$
	perprag.3	$⊢ φ \to C \in (A L B)$
	perprag.4	$⊢ φ \to D \in P$
	perprag.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (C L D)$
Assertion	perprag	$⊢ φ \to ⟨“ A C D ”⟩ \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		perprag.1	$⊢ φ \to A \in P$
7		perprag.2	$⊢ φ \to B \in P$
8		perprag.3	$⊢ φ \to C \in (A L B)$
9		perprag.4	$⊢ φ \to D \in P$
10		perprag.5	$⊢ φ \to (A L B) ⟂_{𝒢} (G) (C L D)$
11		eqidd	$⊢ (φ \land C = D) \to A = A$
12		simpr	$⊢ (φ \land C = D) \to C = D$
13		eqidd	$⊢ (φ \land C = D) \to D = D$
14	11 12 13	s3eqd	$⊢ (φ \land C = D) \to ⟨“ A C D ”⟩ = ⟨“ A D D ”⟩$
15		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
16	1 2 3 4 15 5 6 9 9	ragtrivb	$⊢ φ \to ⟨“ A D D ”⟩ \in ∟_{𝒢} (G)$
17	16	adantr	$⊢ (φ \land C = D) \to ⟨“ A D D ”⟩ \in ∟_{𝒢} (G)$
18	14 17	eqeltrd	$⊢ (φ \land C = D) \to ⟨“ A C D ”⟩ \in ∟_{𝒢} (G)$
19	5	adantr	$⊢ (φ \land C \neq D) \to G \in 𝒢_{Tarski}$
20	1 4 3 5 6 7 8	tglngne	$⊢ φ \to A \neq B$
21	1 3 4 5 6 7 20	tgelrnln	$⊢ φ \to A L B \in ran L$
22	21	adantr	$⊢ (φ \land C \neq D) \to A L B \in ran L$
23	1 4 3 5 21 8	tglnpt	$⊢ φ \to C \in P$
24	23	adantr	$⊢ (φ \land C \neq D) \to C \in P$
25	9	adantr	$⊢ (φ \land C \neq D) \to D \in P$
26		simpr	$⊢ (φ \land C \neq D) \to C \neq D$
27	1 3 4 19 24 25 26	tgelrnln	$⊢ (φ \land C \neq D) \to C L D \in ran L$
28	8	adantr	$⊢ (φ \land C \neq D) \to C \in (A L B)$
29	1 3 4 19 24 25 26	tglinerflx1	$⊢ (φ \land C \neq D) \to C \in (C L D)$
30	28 29	elind	$⊢ (φ \land C \neq D) \to C \in ((A L B) \cap (C L D))$
31	1 3 4 5 6 7 20	tglinerflx1	$⊢ φ \to A \in (A L B)$
32	31	adantr	$⊢ (φ \land C \neq D) \to A \in (A L B)$
33	1 3 4 19 24 25 26	tglinerflx2	$⊢ (φ \land C \neq D) \to D \in (C L D)$
34	10	adantr	$⊢ (φ \land C \neq D) \to (A L B) ⟂_{𝒢} (G) (C L D)$
35	1 2 3 4 19 22 27 30 32 33 34	isperp2d	$⊢ (φ \land C \neq D) \to ⟨“ A C D ”⟩ \in ∟_{𝒢} (G)$
36	18 35	pm2.61dane	$⊢ φ \to ⟨“ A C D ”⟩ \in ∟_{𝒢} (G)$

Metamath Proof Explorer

Theorem perprag

Proof