Metamath Proof Explorer

Theorem tgaaddcpbllem3

Description: Lemma for tgaaddcpbl . (Contributed by Thierry Arnoux, 2-Aug-2026)

Ref Expression
Hypotheses tgaaddcpbl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgaaddcpbl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgaaddcpbl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgaaddcpbl.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
tgaaddcpbl.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
tgaaddcpbl.q ⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
tgaaddcpbl.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgaaddcpbl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
tgaaddcpbl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
tgaaddcpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
tgaaddcpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
tgaaddcpbl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
tgaaddcpbl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tgaaddcpbl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgaaddcpbl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
tgaaddcpbl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
tgaaddcpbl.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
tgaaddcpbl.4 ⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
tgaaddcpbl.5 ⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
tgaaddcpbl.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
tgaaddcpbl.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
tgaaddcpbllem3.1 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
Assertion tgaaddcpbllem3 ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )

Proof

Step Hyp Ref Expression
1 tgaaddcpbl.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgaaddcpbl.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgaaddcpbl.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tgaaddcpbl.c ⊢ ∼ = ( cgrA ‘ 𝐺 )
5 tgaaddcpbl.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) }
6 tgaaddcpbl.q ⊢ 𝑄 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( ( 𝑐 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ∧ 𝑑 ∈ ( 𝑃 ∖ ( 𝑉 𝐿 𝑇 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝑉 𝐿 𝑇 ) 𝑡 ∈ ( 𝑐 𝐼 𝑑 ) ) }
7 tgaaddcpbl.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 tgaaddcpbl.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑃 )
9 tgaaddcpbl.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
10 tgaaddcpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
11 tgaaddcpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑃 )
12 tgaaddcpbl.w ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
13 tgaaddcpbl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
14 tgaaddcpbl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
15 tgaaddcpbl.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
16 tgaaddcpbl.2 ⊢ ( 𝜑 → 𝑌 ≠ 𝑆 )
17 tgaaddcpbl.3 ⊢ ( 𝜑 → 𝑉 ≠ 𝑇 )
18 tgaaddcpbl.4 ⊢ ( 𝜑 → 𝑋 𝑂 𝑍 )
19 tgaaddcpbl.5 ⊢ ( 𝜑 → 𝑈 𝑄 𝑊 )
20 tgaaddcpbl.6 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
21 tgaaddcpbl.7 ⊢ ( 𝜑 → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
22 tgaaddcpbllem3.1 ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
23 eleq1w ⊢ ( 𝑠 = 𝑟 → ( 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ 𝑟 ∈ ( 𝑎 𝐼 𝑏 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ↔ ∃ 𝑟 ∈ ( 𝑌 𝐿 𝑆 ) 𝑟 ∈ ( 𝑎 𝐼 𝑏 ) )
25 24 anbi2i ⊢ ( ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑟 ∈ ( 𝑌 𝐿 𝑆 ) 𝑟 ∈ ( 𝑎 𝐼 𝑏 ) ) )
26 25 opabbii ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑎 𝐼 𝑏 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑟 ∈ ( 𝑌 𝐿 𝑆 ) 𝑟 ∈ ( 𝑎 𝐼 𝑏 ) ) }
27 5 26 eqtri ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑆 ) ) ) ∧ ∃ 𝑟 ∈ ( 𝑌 𝐿 𝑆 ) 𝑟 ∈ ( 𝑎 𝐼 𝑏 ) ) }
28 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝐺 ∈ TarskiG )
29 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑆 ∈ 𝑃 )
30 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑇 ∈ 𝑃 )
31 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑈 ∈ 𝑃 )
32 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑉 ∈ 𝑃 )
33 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑊 ∈ 𝑃 )
34 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑋 ∈ 𝑃 )
35 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑌 ∈ 𝑃 )
36 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑍 ∈ 𝑃 )
37 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑌 ≠ 𝑆 )
38 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑉 ≠ 𝑇 )
39 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑋 𝑂 𝑍 )
40 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑈 𝑄 𝑊 )
41 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
42 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
43 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
44 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
45 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) )
46 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) )
47 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 )
48 1 2 3 4 27 6 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 tgaaddcpbllem1 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
49 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝐺 ∈ TarskiG )
50 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑆 ∈ 𝑃 )
51 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑇 ∈ 𝑃 )
52 10 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑈 ∈ 𝑃 )
53 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑉 ∈ 𝑃 )
54 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑊 ∈ 𝑃 )
55 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑋 ∈ 𝑃 )
56 14 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑌 ∈ 𝑃 )
57 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑍 ∈ 𝑃 )
58 16 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑌 ≠ 𝑆 )
59 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑉 ≠ 𝑇 )
60 18 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑋 𝑂 𝑍 )
61 19 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑈 𝑄 𝑊 )
62 20 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → ⟨“ 𝑋 𝑌 𝑆 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑇 ”⟩ )
63 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → ⟨“ 𝑆 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑇 𝑉 𝑊 ”⟩ )
64 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → ¬ 𝑌 ∈ ( 𝑋 𝐼 𝑍 ) )
65 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) )
66 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) )
67 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) )
68 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑉 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑉 )
69 1 2 3 4 27 6 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 44 tgaaddcpbllem2 ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ∧ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
70 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑆 ∈ 𝑃 )
71 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑌 ∈ 𝑃 )
72 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝐺 ∈ TarskiG )
73 1 2 3 7 14 8 16 tgelrnln ⊢ ( 𝜑 → ( 𝑌 𝐿 𝑆 ) ∈ ran 𝐿 )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑌 𝐿 𝑆 ) ∈ ran 𝐿 )
75 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) )
76 1 3 2 72 74 75 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑠 ∈ 𝑃 )
77 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑋 ∈ 𝑃 )
78 16 necomd ⊢ ( 𝜑 → 𝑆 ≠ 𝑌 )
79 78 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑆 ≠ 𝑌 )
80 1 2 3 72 70 71 76 79 75 lncom ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → 𝑠 ∈ ( 𝑆 𝐿 𝑌 ) )
81 1 2 44 70 71 76 72 77 3 80 lnhl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → ( 𝑠 ( ( hlG ‘ 𝐺 ) ‘ 𝑌 ) 𝑆 ∨ 𝑌 ∈ ( 𝑆 𝐼 𝑠 ) ) )
82 48 69 81 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )
83 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
84 1 83 2 5 13 15 islnopp ⊢ ( 𝜑 → ( 𝑋 𝑂 𝑍 ↔ ( ( ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) ) )
85 18 84 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝑋 ∈ ( 𝑌 𝐿 𝑆 ) ∧ ¬ 𝑍 ∈ ( 𝑌 𝐿 𝑆 ) ) ∧ ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) ) )
86 85 simprd ⊢ ( 𝜑 → ∃ 𝑠 ∈ ( 𝑌 𝐿 𝑆 ) 𝑠 ∈ ( 𝑋 𝐼 𝑍 ) )
87 82 86 r19.29a ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∼ ⟨“ 𝑈 𝑉 𝑊 ”⟩ )