Metamath Proof Explorer

Theorem perpprlng

Description: If two lines A and B have a common perpendicular C and lie in the same plane H , then they are parallel. Theorem 12.9 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses perpprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
perpprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
perpprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
perpprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
perpprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
perpprlng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
perpprlng.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
perpprlng.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
perpprlng.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
perpprlng.q ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐶 )
perpprlng.2 ⊢ ( 𝜑 → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
Assertion perpprlng ( 𝜑 → 𝐴 ∥ 𝐵 )

Proof

Step Hyp Ref Expression
1 perpprlng.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 perpprlng.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 perpprlng.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
4 perpprlng.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
5 perpprlng.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 perpprlng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 perpprlng.a ⊢ ( 𝜑 → 𝐴 ⊆ 𝐻 )
8 perpprlng.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐻 )
9 perpprlng.1 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐻 )
10 perpprlng.q ⊢ ( 𝜑 → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐶 )
11 perpprlng.2 ⊢ ( 𝜑 → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐺 ∈ TarskiG )
13 2 5 10 perpln1 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ ran 𝐿 )
15 2 5 11 perpln1 ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ∈ ran 𝐿 )
17 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐻 ∈ ran 𝐸 )
18 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ⊆ 𝐻 )
19 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐵 ⊆ 𝐻 )
20 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
21 2 3 4 12 14 16 17 18 19 20 prlngd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∥ 𝐵 )
22 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → 𝐺 ∈ TarskiG )
23 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → 𝐴 ∈ ran 𝐿 )
24 2 3 4 22 23 prlngref ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → 𝐴 ∥ 𝐴 )
25 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
26 5 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
27 2 5 10 perpln2 ⊢ ( 𝜑 → 𝐶 ∈ ran 𝐿 )
28 27 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐶 ∈ ran 𝐿 )
29 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐻 ∈ ran 𝐸 )
30 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ∈ 𝐶 )
31 9 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐶 ⊆ 𝐻 )
32 7 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐴 ⊆ 𝐻 )
33 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) )
34 33 eldifad ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ∈ 𝐴 )
35 32 34 sseldd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ∈ 𝐻 )
36 8 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐵 ⊆ 𝐻 )
37 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
38 37 eldifad ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑦 ∈ 𝐵 )
39 36 38 sseldd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑦 ∈ 𝐻 )
40 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
41 13 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐴 ∈ ran 𝐿 )
42 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
43 42 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
44 43 elin1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ∈ 𝐴 )
45 1 2 40 26 41 44 tglnpt ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ∈ 𝑃 )
46 1 2 40 26 41 34 tglnpt ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ∈ 𝑃 )
47 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑧 ≠ 𝑥 )
48 47 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝑥 ≠ 𝑧 )
49 1 40 2 26 45 46 48 48 41 44 34 tglinethru ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐴 = ( 𝑥 𝐿 𝑧 ) )
50 10 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐶 )
51 49 50 eqbrtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → ( 𝑥 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐶 )
52 22 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐺 ∈ TarskiG )
53 52 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
54 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ∈ ran 𝐿 )
55 54 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐵 ∈ ran 𝐿 )
56 42 elin2d ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
57 56 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑥 ∈ 𝐵 )
58 1 2 40 53 55 57 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑥 ∈ 𝑃 )
59 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) )
60 59 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑦 ∈ 𝐵 )
61 1 2 40 53 55 60 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑦 ∈ 𝑃 )
62 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑦 ≠ 𝑥 )
63 62 necomd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑥 ≠ 𝑦 )
64 1 40 2 53 58 61 63 63 55 57 60 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
65 64 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
66 65 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐵 = ( 𝑥 𝐿 𝑦 ) )
67 11 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
68 66 67 eqbrtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → ( 𝑥 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐶 )
69 1 2 3 26 28 29 30 31 35 39 51 68 perpeq ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → ( 𝑥 𝐿 𝑧 ) = ( 𝑥 𝐿 𝑦 ) )
70 69 49 66 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) ∧ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) ) ∧ 𝑧 ≠ 𝑥 ) → 𝐴 = 𝐵 )
71 23 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐴 ∈ ran 𝐿 )
72 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐶 ∈ ran 𝐿 )
73 72 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐶 ∈ ran 𝐿 )
74 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
75 74 elin1d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝑥 ∈ 𝐴 )
76 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
77 1 76 40 2 5 13 27 10 perpneq ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
78 77 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐴 ≠ 𝐶 )
79 1 40 2 53 71 73 75 78 tglnpt4 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) 𝑧 ≠ 𝑥 )
80 79 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐶 ) 𝑧 ≠ 𝑥 )
81 70 80 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) ) ∧ 𝑦 ≠ 𝑥 ) → 𝐴 = 𝐵 )
82 1 76 40 2 5 15 27 11 perpneq ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
83 82 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ≠ 𝐶 )
84 1 40 2 52 54 72 56 83 tglnpt4 ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) 𝑦 ≠ 𝑥 )
85 84 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) → ∃ 𝑦 ∈ ( 𝐵 ∖ 𝐶 ) 𝑦 ≠ 𝑥 )
86 81 85 r19.29a ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑥 ∈ 𝐶 ) → 𝐴 = 𝐵 )
87 52 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝐺 ∈ TarskiG )
88 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐶 )
89 87 88 perpin ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
90 87 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐺 ∈ TarskiG )
91 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
92 91 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
93 90 92 perpin ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) → ( 𝐵 ∩ 𝐶 ) ≠ ∅ )
94 90 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐺 ∈ TarskiG )
95 72 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐶 ∈ ran 𝐿 )
96 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) )
97 96 elin2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ 𝐶 )
98 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) )
99 98 elin2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ∈ 𝐶 )
100 23 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ∈ ran 𝐿 )
101 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) )
102 101 elin1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐴 )
103 1 2 40 94 100 102 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ∈ 𝑃 )
104 1 2 40 94 95 97 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ 𝑃 )
105 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → ¬ 𝑥 ∈ 𝐶 )
106 nelne2 ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝑦 ≠ 𝑥 )
107 97 105 106 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 ≠ 𝑥 )
108 96 elin1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 ∈ 𝐴 )
109 1 40 2 94 104 103 107 107 100 108 102 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 = ( 𝑦 𝐿 𝑥 ) )
110 88 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 ( ⟂G ‘ 𝐺 ) 𝐶 )
111 109 110 eqbrtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑦 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐶 )
112 1 2 40 94 95 99 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ∈ 𝑃 )
113 nelne2 ⊢ ( ( 𝑧 ∈ 𝐶 ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝑧 ≠ 𝑥 )
114 99 105 113 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ≠ 𝑥 )
115 54 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐵 ∈ ran 𝐿 )
116 98 elin1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑧 ∈ 𝐵 )
117 56 ad3antrrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ∈ 𝐵 )
118 1 40 2 94 112 103 114 114 115 116 117 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐵 = ( 𝑧 𝐿 𝑥 ) )
119 92 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐵 ( ⟂G ‘ 𝐺 ) 𝐶 )
120 118 119 eqbrtrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑧 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐶 )
121 1 76 40 2 94 95 97 99 103 111 120 footeq ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑦 = 𝑧 )
122 121 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑥 𝐿 𝑧 ) )
123 107 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ≠ 𝑦 )
124 1 40 2 94 103 104 123 123 100 102 108 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
125 114 necomd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝑥 ≠ 𝑧 )
126 1 40 2 94 103 112 125 125 115 117 116 tglinethru ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐵 = ( 𝑥 𝐿 𝑧 ) )
127 122 124 126 3eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) ∧ 𝑧 ∈ ( 𝐵 ∩ 𝐶 ) ) → 𝐴 = 𝐵 )
128 93 127 n0limd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐶 ) ) → 𝐴 = 𝐵 )
129 89 128 n0limd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ ¬ 𝑥 ∈ 𝐶 ) → 𝐴 = 𝐵 )
130 86 129 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐴 = 𝐵 )
131 25 130 n0limd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → 𝐴 = 𝐵 )
132 24 131 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → 𝐴 ∥ 𝐵 )
133 21 132 pm2.61dane ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )