Metamath Proof Explorer

Theorem perpneq

Description: Two perpendicular lines are different. Theorem 8.14 of Schwabhauser p. 59. (Contributed by Thierry Arnoux, 18-Oct-2019)

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
perpcom.1 ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
Assertion perpneq ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isperp.d ⊢ − = ( dist ‘ 𝐺 )
3 isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 isperp.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
8 perpcom.1 ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐺 ∈ TarskiG )
10 9 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐺 ∈ TarskiG )
11 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐺 ∈ TarskiG )
12 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐴 ∈ ran 𝐿 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
14 13 elin1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
15 14 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ∈ 𝐴 )
16 1 4 3 11 12 15 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ∈ 𝑃 )
17 16 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ∈ 𝑃 )
18 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐵 ∈ ran 𝐿 )
19 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ∈ 𝐵 )
20 1 4 3 11 18 19 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ∈ 𝑃 )
21 20 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ∈ 𝑃 )
22 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ∈ 𝐴 )
23 1 4 3 11 12 22 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ∈ 𝑃 )
24 23 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ∈ 𝑃 )
25 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
26 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ∈ 𝐴 )
27 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ∈ 𝐵 )
28 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
29 id ⊢ ( 𝑦 = 𝑢 → 𝑦 = 𝑢 )
30 eqidd ⊢ ( 𝑦 = 𝑢 → 𝑥 = 𝑥 )
31 eqidd ⊢ ( 𝑦 = 𝑢 → 𝑧 = 𝑧 )
32 29 30 31 s3eqd ⊢ ( 𝑦 = 𝑢 → ⟨“ 𝑦 𝑥 𝑧 ”⟩ = ⟨“ 𝑢 𝑥 𝑧 ”⟩ )
33 32 eleq1d ⊢ ( 𝑦 = 𝑢 → ( ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑢 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
34 eqidd ⊢ ( 𝑧 = 𝑣 → 𝑢 = 𝑢 )
35 eqidd ⊢ ( 𝑧 = 𝑣 → 𝑥 = 𝑥 )
36 id ⊢ ( 𝑧 = 𝑣 → 𝑧 = 𝑣 )
37 34 35 36 s3eqd ⊢ ( 𝑧 = 𝑣 → ⟨“ 𝑢 𝑥 𝑧 ”⟩ = ⟨“ 𝑢 𝑥 𝑣 ”⟩ )
38 37 eleq1d ⊢ ( 𝑧 = 𝑣 → ( ⟨“ 𝑢 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
39 33 38 rspc2va ⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
40 26 27 28 39 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ⟨“ 𝑢 𝑥 𝑣 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
41 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ≠ 𝑢 )
42 41 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ≠ 𝑥 )
43 42 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑢 ≠ 𝑥 )
44 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ≠ 𝑣 )
45 44 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ≠ 𝑥 )
46 45 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑣 ≠ 𝑥 )
47 1 2 3 4 25 10 24 17 21 40 43 46 ragncol ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ¬ ( 𝑣 ∈ ( 𝑢 𝐿 𝑥 ) ∨ 𝑢 = 𝑥 ) )
48 1 4 3 10 24 17 21 47 ncolrot2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ¬ ( 𝑥 ∈ ( 𝑣 𝐿 𝑢 ) ∨ 𝑣 = 𝑢 ) )
49 1 3 4 10 17 21 24 17 48 tglineneq ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ( 𝑥 𝐿 𝑣 ) ≠ ( 𝑢 𝐿 𝑥 ) )
50 49 necomd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → ( 𝑢 𝐿 𝑥 ) ≠ ( 𝑥 𝐿 𝑣 ) )
51 1 3 4 11 23 16 42 42 12 22 15 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐴 = ( 𝑢 𝐿 𝑥 ) )
52 51 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐴 = ( 𝑢 𝐿 𝑥 ) )
53 13 elin2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
54 53 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝑥 ∈ 𝐵 )
55 1 3 4 11 16 20 44 44 18 54 19 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐵 = ( 𝑥 𝐿 𝑣 ) )
56 55 adantl4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐵 = ( 𝑥 𝐿 𝑣 ) )
57 50 52 56 3netr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑥 ≠ 𝑣 ) → 𝐴 ≠ 𝐵 )
58 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ∈ ran 𝐿 )
59 1 3 4 9 58 53 tglnpt2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑣 ∈ 𝐵 𝑥 ≠ 𝑣 )
60 59 ad5ant12 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) → ∃ 𝑣 ∈ 𝐵 𝑥 ≠ 𝑣 )
61 57 60 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑢 ) → 𝐴 ≠ 𝐵 )
62 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐴 ∈ ran 𝐿 )
63 1 3 4 9 62 14 tglnpt2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑢 ∈ 𝐴 𝑥 ≠ 𝑢 )
64 63 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → ∃ 𝑢 ∈ 𝐴 𝑥 ≠ 𝑢 )
65 61 64 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) → 𝐴 ≠ 𝐵 )
66 1 2 3 4 5 6 7 isperp ⊢ ( 𝜑 → ( 𝐴 ( ⟂G ‘ 𝐺 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ) )
67 8 66 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ⟨“ 𝑦 𝑥 𝑧 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
68 65 67 r19.29a ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )