Metamath Proof Explorer

Theorem perpeqlem

Description: Lemma for perpeq . (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses perpeq.1 ⊢ 𝑃 = ( Base ‘ 𝐺 )
perpeq.2 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
perpeq.3 ⊢ 𝐸 = ( hlG ‘ 𝐺 )
perpeq.4 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
perpeq.5 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
perpeq.6 ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
perpeq.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
perpeq.8 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
perpeq.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
perpeq.10 ⊢ ( 𝜑 → 𝑍 ∈ 𝐻 )
perpeq.11 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
perpeq.12 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
perpeqlem.1 ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
Assertion perpeqlem ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 𝐿 𝑍 ) )

Proof

Step Hyp Ref Expression
1 perpeq.1 ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 perpeq.2 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 perpeq.3 ⊢ 𝐸 = ( hlG ‘ 𝐺 )
4 perpeq.4 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 perpeq.5 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6 perpeq.6 ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 perpeq.7 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8 perpeq.8 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
9 perpeq.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
10 perpeq.10 ⊢ ( 𝜑 → 𝑍 ∈ 𝐻 )
11 perpeq.11 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
12 perpeq.12 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
13 perpeqlem.1 ⊢ ( 𝜑 → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
14 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
15 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝐺 ∈ TarskiG )
16 1 2 14 4 5 7 tglnpt ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ∈ 𝑃 )
18 1 14 2 3 4 6 9 plngrnssp ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ∈ 𝑃 )
20 2 4 11 perpln1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
21 1 14 2 4 16 18 20 tglnne ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ≠ 𝑌 )
23 2 4 12 perpln1 ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
25 1 14 2 3 4 6 10 plngrnssp ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
26 1 14 2 4 16 25 23 tglnne ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )
27 26 necomd ⊢ ( 𝜑 → 𝑍 ≠ 𝑋 )
28 1 14 2 4 25 16 27 tglinerflx2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑍 𝐿 𝑋 ) )
29 1 14 2 4 16 25 26 tglinecom ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
30 28 29 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) )
32 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
33 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑍 ∈ 𝑃 )
34 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝐴 ∈ ran 𝐿 )
35 simplr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) )
36 35 eldifad ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑡 ∈ 𝐴 )
37 1 2 14 15 34 36 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑡 ∈ 𝑃 )
38 simpr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑡 ≠ 𝑋 )
39 38 necomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ≠ 𝑡 )
40 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
41 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
42 21 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
43 1 14 2 4 18 16 42 tglinerflx2 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑋 ) )
45 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑌 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
46 1 14 2 15 17 19 22 tglinecom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑋 ) )
47 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ∈ 𝐴 )
48 1 14 2 15 17 37 39 39 34 47 36 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝐴 = ( 𝑋 𝐿 𝑡 ) )
49 45 46 48 3brtr3d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑌 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑡 ) )
50 1 40 14 2 15 19 17 44 37 49 perprag ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ⟨“ 𝑌 𝑋 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
51 1 40 14 2 41 15 19 17 37 50 ragcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ⟨“ 𝑡 𝑋 𝑌 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
52 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑋 ∈ ( 𝑍 𝐿 𝑋 ) )
53 29 12 eqbrtrrd ⊢ ( 𝜑 → ( 𝑍 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
54 53 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑍 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
55 54 48 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑍 𝐿 𝑋 ) ( ⟂G ‘ 𝐺 ) ( 𝑋 𝐿 𝑡 ) )
56 1 40 14 2 15 33 17 52 37 55 perprag ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ⟨“ 𝑍 𝑋 𝑡 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
57 1 40 14 2 41 15 33 17 37 56 ragcom ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ⟨“ 𝑡 𝑋 𝑍 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
58 1 14 2 15 37 17 38 38 34 36 47 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝐴 = ( 𝑡 𝐿 𝑋 ) )
59 58 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) = ( ( hpG ‘ 𝐺 ) ‘ ( 𝑡 𝐿 𝑋 ) ) )
60 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑍 )
61 59 60 breqdi ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ( ( hpG ‘ 𝐺 ) ‘ ( 𝑡 𝐿 𝑋 ) ) 𝑍 )
62 1 2 15 17 37 19 33 39 51 57 61 ragraghl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ( ( hlG ‘ 𝐺 ) ‘ 𝑋 ) 𝑍 )
63 1 14 32 19 33 17 15 2 62 hlln ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ∈ ( 𝑍 𝐿 𝑋 ) )
64 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑍 𝐿 𝑋 ) )
65 63 64 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) )
66 1 14 2 15 17 19 22 22 24 31 65 tglinethru ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑍 ) = ( 𝑋 𝐿 𝑌 ) )
67 66 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) ) ∧ 𝑡 ≠ 𝑋 ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 𝐿 𝑍 ) )
68 1 40 14 2 4 20 5 11 perpneq ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) ≠ 𝐴 )
69 68 necomd ⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
70 1 14 2 4 5 20 7 69 tglnpt4 ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( 𝐴 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝑡 ≠ 𝑋 )
71 67 70 r19.29a ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑋 𝐿 𝑍 ) )