Theorem 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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	colperpex.d	⊢ − = ( dist ‘ 𝐺 )
	colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	perpdrag.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	perpdrag.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	perpdrag.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	perpdrag.4	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
Assertion	perpdragALT	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		colperpex.d	⊢ − = ( dist ‘ 𝐺 )
3		colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		perpdrag.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
7		perpdrag.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
8		perpdrag.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		perpdrag.4	⊢ ( 𝜑 → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
10		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐴 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
12		eqidd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐶 = 𝐶 )
13	10 11 12	s3eqd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ 𝐴 𝐴 𝐶 ”⟩ = ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
14		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
15	4 5 9	perpln1	⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
16	1 4 3 5 15 6	tglnpt	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
17	1 2 3 4 14 5 8 16 8	ragtrivb	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐴 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
18	1 2 3 4 14 5 8 16 16 17	ragcom	⊢ ( 𝜑 → ⟨“ 𝐴 𝐴 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ 𝐴 𝐴 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
20	13 19	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
21	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
22	16	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
23	1 4 3 5 15 7	tglnpt	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
25	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝐷 )
26		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
27	15	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ∈ ran 𝐿 )
28	6	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝐷 )
29	1 3 4 21 22 24 26 26 27 28 25	tglinethru	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 = ( 𝐴 𝐿 𝐵 ) )
30	25 29	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝐴 𝐿 𝐵 ) )
31	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐶 ∈ 𝑃 )
32	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
33	29 32	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐶 ) )
34	1 2 3 4 21 22 24 30 31 33	perprag	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
35	20 34	pm2.61dane	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )