Metamath Proof Explorer

Theorem prlngmolem2

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

Ref Expression
Hypotheses prlngeu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
prlngeu.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
prlngeu.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlngeu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlngeu.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
prlngeu.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
prlngeu.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
prlngmolem2.1 ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑟 ∈ 𝑏 𝑟 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) }
prlngmolem2.2 ⊢ 𝑄 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) }
Assertion prlngmolem2 ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )

Proof

Step Hyp Ref Expression
1 prlngeu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 prlngeu.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 prlngeu.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 prlngeu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 prlngeu.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6 prlngeu.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
7 prlngeu.1 ⊢ ( 𝜑 → 𝐺 ∈ TarskiGE )
8 prlngmolem2.1 ⊢ 𝑂 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝑏 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝑏 ) ) ∧ ∃ 𝑟 ∈ 𝑏 𝑟 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) }
9 prlngmolem2.2 ⊢ 𝑄 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑦 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑠 ∈ 𝐴 𝑠 ∈ ( 𝑥 ( Itv ‘ 𝐺 ) 𝑦 ) ) }
10 anass ⊢ ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) ↔ ( 𝐴 ∥ 𝑏 ∧ ( 𝑋 ∈ 𝑏 ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) ) )
11 4 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) → 𝐺 ∈ TarskiG )
12 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) → 𝐴 ∈ ran 𝐿 )
13 2 11 12 tglnne0 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) → 𝐴 ≠ ∅ )
14 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 = 𝑐 ) → 𝑏 = 𝑐 )
15 7 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝐺 ∈ TarskiGE )
16 11 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝐺 ∈ TarskiG )
17 16 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝐺 ∈ TarskiG )
18 12 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝐴 ∈ ran 𝐿 )
19 6 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
20 19 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
21 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
22 simp-8r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑏 ∈ ran 𝐿 )
23 22 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑏 ∈ ran 𝐿 )
24 simp-7r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑐 ∈ ran 𝐿 )
25 24 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑐 ∈ ran 𝐿 )
26 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝐴 ∥ 𝑏 )
27 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝐴 ∥ 𝑐 )
28 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑋 ∈ 𝑏 )
29 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑋 ∈ 𝑐 )
30 29 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑋 ∈ 𝑐 )
31 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑡 ∈ 𝐴 )
32 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) )
33 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑏 ≠ 𝑐 )
34 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → 𝑤 𝑂 𝑡 )
35 1 2 3 17 18 20 8 9 21 23 25 26 27 28 30 31 32 33 34 prlngmolem1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑤 𝑂 𝑡 ) → ¬ 𝐺 ∈ TarskiGE )
36 16 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝐺 ∈ TarskiG )
37 12 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝐴 ∈ ran 𝐿 )
38 19 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
39 22 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑏 ∈ ran 𝐿 )
40 24 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑐 ∈ ran 𝐿 )
41 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝐴 ∥ 𝑏 )
42 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝐴 ∥ 𝑐 )
43 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑋 ∈ 𝑏 )
44 29 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑋 ∈ 𝑐 )
45 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑡 ∈ 𝐴 )
46 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
47 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
48 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 )
49 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) )
50 49 eldifad ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ 𝑐 )
51 50 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑤 ∈ 𝑐 )
52 1 46 21 2 47 36 48 40 44 51 mirln ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑐 )
53 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) )
54 53 eldifbd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ¬ 𝑤 ∈ 𝑏 )
55 36 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝐺 ∈ TarskiG )
56 1 2 21 16 24 29 tglnpt ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑋 ∈ 𝑃 )
57 56 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝑋 ∈ 𝑃 )
58 16 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐺 ∈ TarskiG )
59 24 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑐 ∈ ran 𝐿 )
60 1 2 21 58 59 50 tglnpt ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ 𝑃 )
61 60 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝑤 ∈ 𝑃 )
62 1 46 21 2 47 55 57 48 61 mirmir ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ) = 𝑤 )
63 39 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝑏 ∈ ran 𝐿 )
64 43 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝑋 ∈ 𝑏 )
65 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 )
66 1 46 21 2 47 55 48 63 64 65 mirln ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ) ∈ 𝑏 )
67 62 66 eqeltrrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 ) → 𝑤 ∈ 𝑏 )
68 54 67 mtand ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ 𝑏 )
69 52 68 eldifd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) ∈ ( 𝑐 ∖ 𝑏 ) )
70 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → 𝑏 ≠ 𝑐 )
71 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 )
72 1 2 3 36 37 38 8 9 21 39 40 41 42 43 44 45 69 70 71 prlngmolem1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) → ¬ 𝐺 ∈ TarskiGE )
73 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
74 22 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑏 ∈ ran 𝐿 )
75 49 eldifbd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ¬ 𝑤 ∈ 𝑏 )
76 60 75 eldifd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ ( 𝑃 ∖ 𝑏 ) )
77 12 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ∈ ran 𝐿 )
78 6 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
79 1 21 2 73 58 77 78 elplnglnid ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ⊆ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
80 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑡 ∈ 𝐴 )
81 79 80 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑡 ∈ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
82 1 2 73 58 77 78 tgelrnpln ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) ∈ ran ( hlG ‘ 𝐺 ) )
83 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ∥ 𝑐 )
84 29 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑋 ∈ 𝑐 )
85 6 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
86 85 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ¬ 𝑋 ∈ 𝐴 )
87 nelne1 ⊢ ( ( 𝑋 ∈ 𝑐 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑐 ≠ 𝐴 )
88 84 86 87 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑐 ≠ 𝐴 )
89 88 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ≠ 𝑐 )
90 2 73 3 58 83 89 50 84 prlnghpg ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
91 1 2 73 77 60 78 58 90 hpgssplng ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
92 91 75 eldifd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑤 ∈ ( ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) ∖ 𝑏 ) )
93 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ∥ 𝑏 )
94 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑋 ∈ 𝑏 )
95 nelne1 ⊢ ( ( 𝑋 ∈ 𝑏 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝑏 ≠ 𝐴 )
96 94 86 95 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑏 ≠ 𝐴 )
97 96 necomd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝐴 ≠ 𝑏 )
98 2 73 3 58 93 97 94 prlngpln3 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑏 ⊆ ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) )
99 1 2 73 58 82 74 92 98 plng3p ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ( 𝐴 ( hlG ‘ 𝐺 ) 𝑋 ) = ( 𝑏 ( hlG ‘ 𝐺 ) 𝑤 ) )
100 81 99 eleqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑡 ∈ ( 𝑏 ( hlG ‘ 𝐺 ) 𝑤 ) )
101 2 3 58 93 97 prlngin0 ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ( 𝐴 ∩ 𝑏 ) = ∅ )
102 101 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → ( 𝐴 ∩ 𝑏 ) = ∅ )
103 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → 𝑡 ∈ 𝐴 )
104 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → 𝑡 ∈ 𝑏 )
105 103 104 elind ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → 𝑡 ∈ ( 𝐴 ∩ 𝑏 ) )
106 105 ne0d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → ( 𝐴 ∩ 𝑏 ) ≠ ∅ )
107 106 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) ∧ 𝑡 ∈ 𝑏 ) → ¬ ( 𝐴 ∩ 𝑏 ) = ∅ )
108 102 107 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ¬ 𝑡 ∈ 𝑏 )
109 100 108 eldifd ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → 𝑡 ∈ ( ( 𝑏 ( hlG ‘ 𝐺 ) 𝑤 ) ∖ 𝑏 ) )
110 1 21 2 73 47 48 8 58 74 76 109 94 plngmiropp ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ( 𝑤 𝑂 𝑡 ∨ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑋 ) ‘ 𝑤 ) 𝑂 𝑡 ) )
111 35 72 110 mpjaodan ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) ∧ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) ) ∧ 𝑤 ≠ 𝑋 ) → ¬ 𝐺 ∈ TarskiGE )
112 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑏 ≠ 𝑐 )
113 112 necomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑐 ≠ 𝑏 )
114 1 21 2 16 24 22 29 113 tglnpt4 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → ∃ 𝑤 ∈ ( 𝑐 ∖ 𝑏 ) 𝑤 ≠ 𝑋 )
115 111 114 r19.29a ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → ¬ 𝐺 ∈ TarskiGE )
116 15 115 pm2.21dd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) ∧ 𝑏 ≠ 𝑐 ) → 𝑏 = 𝑐 )
117 14 116 pm2.61dane ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) ∧ 𝑡 ∈ 𝐴 ) → 𝑏 = 𝑐 )
118 13 117 n0limd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ 𝐴 ∥ 𝑐 ) ∧ 𝑋 ∈ 𝑐 ) → 𝑏 = 𝑐 )
119 118 anasss ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) → 𝑏 = 𝑐 )
120 119 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ 𝐴 ∥ 𝑏 ) ∧ ( 𝑋 ∈ 𝑏 ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) ) → 𝑏 = 𝑐 )
121 120 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ ( 𝐴 ∥ 𝑏 ∧ ( 𝑋 ∈ 𝑏 ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) ) ) → 𝑏 = 𝑐 )
122 10 121 sylan2b ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) ∧ ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) ) → 𝑏 = 𝑐 )
123 122 ex ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) ∧ 𝑐 ∈ ran 𝐿 ) → ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) → 𝑏 = 𝑐 ) )
124 123 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐿 ) → ∀ 𝑐 ∈ ran 𝐿 ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) → 𝑏 = 𝑐 ) )
125 124 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ ran 𝐿 ∀ 𝑐 ∈ ran 𝐿 ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) → 𝑏 = 𝑐 ) )
126 breq2 ⊢ ( 𝑏 = 𝑐 → ( 𝐴 ∥ 𝑏 ↔ 𝐴 ∥ 𝑐 ) )
127 eleq2w ⊢ ( 𝑏 = 𝑐 → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ 𝑐 ) )
128 126 127 anbi12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) )
129 128 rmo4 ⊢ ( ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ↔ ∀ 𝑏 ∈ ran 𝐿 ∀ 𝑐 ∈ ran 𝐿 ( ( ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) ∧ ( 𝐴 ∥ 𝑐 ∧ 𝑋 ∈ 𝑐 ) ) → 𝑏 = 𝑐 ) )
130 125 129 sylibr ⊢ ( 𝜑 → ∃* 𝑏 ∈ ran 𝐿 ( 𝐴 ∥ 𝑏 ∧ 𝑋 ∈ 𝑏 ) )