Metamath Proof Explorer

Theorem lnssplnglem

Description: Lemma for lnssplng . (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
lnssplnglem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) )
lnssplnglem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐸 𝑅 ) )
lnssplnglem.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
lnssplnglem.2 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
lnssplnglem.3 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
lnssplnglem.4 ⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
lnssplnglem.5 ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐴 )
Assertion lnssplnglem ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝐴 𝐸 𝑅 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )

Proof

Step Hyp Ref Expression
1 plngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 plngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 plngval.1 ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 plngval.e ⊢ 𝐸 = ( hlG ‘ 𝐺 )
5 plngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 lnssplnglem.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) )
7 lnssplnglem.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 𝐸 𝑅 ) )
8 lnssplnglem.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
9 lnssplnglem.2 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
10 lnssplnglem.3 ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑃 ∖ 𝐴 ) )
11 lnssplnglem.4 ⊢ ( 𝜑 → 𝐴 ≠ ( 𝑋 𝐿 𝑌 ) )
12 lnssplnglem.5 ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐴 )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐺 ∈ TarskiG )
14 13 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
15 1 2 3 4 5 9 10 6 plngssp ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑋 ∈ 𝑃 )
17 1 2 3 4 5 9 10 7 plngssp ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑌 ∈ 𝑃 )
19 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑋 ≠ 𝑌 )
20 1 2 3 13 16 18 19 tgelrnln ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
22 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐴 ∈ ran 𝐿 )
23 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑧 ∈ 𝐴 )
24 1 3 2 14 22 23 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑧 ∈ 𝑃 )
25 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
26 24 25 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑧 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
27 1 2 3 4 14 21 26 elplnglnid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) )
28 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
29 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
30 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
31 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
32 24 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑧 ∈ 𝑃 )
33 19 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑌 )
34 1 2 3 5 15 17 8 tglinerflx2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
35 34 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
36 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
37 nelne2 ⊢ ( ( 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ≠ 𝑧 )
38 35 36 37 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑌 ≠ 𝑧 )
39 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) )
40 1 2 3 29 31 32 30 38 39 lncom ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑌 𝐿 𝑧 ) )
41 1 2 3 29 30 31 32 33 40 38 lnrot2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) ) → 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
42 25 41 mtand ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) )
43 28 42 eldifd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑃 ∖ ( 𝑧 𝐿 𝑌 ) ) )
44 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
45 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑌 )
46 1 2 3 4 14 43 44 26 45 plngrot ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) = ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑋 ) )
47 46 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) = ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑋 ) )
48 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝐺 ∈ TarskiG )
49 24 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑧 ∈ 𝑃 )
50 17 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑌 ∈ 𝑃 )
51 23 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑧 ∈ 𝐴 )
52 12 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ¬ 𝑌 ∈ 𝐴 )
53 nelne2 ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑌 ∈ 𝐴 ) → 𝑧 ≠ 𝑌 )
54 51 52 53 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑧 ≠ 𝑌 )
55 1 2 3 48 49 50 54 tgelrnln ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( 𝑧 𝐿 𝑌 ) ∈ ran 𝐿 )
56 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝐴 ∈ ran 𝐿 )
57 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) )
58 57 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ∈ 𝐴 )
59 1 3 2 48 56 58 tglnpt ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ∈ 𝑃 )
60 57 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ¬ 𝑤 ∈ ( 𝑌 𝐿 𝑧 ) )
61 1 2 3 48 49 50 54 tglinecom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( 𝑧 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑧 ) )
62 60 61 neleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ¬ 𝑤 ∈ ( 𝑧 𝐿 𝑌 ) )
63 59 62 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ∈ ( 𝑃 ∖ ( 𝑧 𝐿 𝑌 ) ) )
64 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑋 ∈ ( 𝐴 𝐸 𝑅 ) )
65 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ≠ 𝑧 )
66 1 2 3 48 59 49 65 65 56 58 51 tglinethru ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝐴 = ( 𝑤 𝐿 𝑧 ) )
67 52 66 neleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ¬ 𝑌 ∈ ( 𝑤 𝐿 𝑧 ) )
68 50 67 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑌 ∈ ( 𝑃 ∖ ( 𝑤 𝐿 𝑧 ) ) )
69 59 60 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑤 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑧 ) ) )
70 54 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑌 ≠ 𝑧 )
71 1 2 3 4 48 68 49 69 70 plngrot ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑌 𝐿 𝑧 ) 𝐸 𝑤 ) = ( ( 𝑤 𝐿 𝑧 ) 𝐸 𝑌 ) )
72 61 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) = ( ( 𝑌 𝐿 𝑧 ) 𝐸 𝑤 ) )
73 66 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( 𝐴 𝐸 𝑌 ) = ( ( 𝑤 𝐿 𝑧 ) 𝐸 𝑌 ) )
74 71 72 73 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) = ( 𝐴 𝐸 𝑌 ) )
75 7 12 eldifd ⊢ ( 𝜑 → 𝑌 ∈ ( ( 𝐴 𝐸 𝑅 ) ∖ 𝐴 ) )
76 1 2 3 4 5 9 10 75 plngcp ⊢ ( 𝜑 → ( 𝐴 𝐸 𝑅 ) = ( 𝐴 𝐸 𝑌 ) )
77 76 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( 𝐴 𝐸 𝑅 ) = ( 𝐴 𝐸 𝑌 ) )
78 74 77 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) = ( 𝐴 𝐸 𝑅 ) )
79 64 78 eleqtrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑋 ∈ ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) )
80 42 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ¬ 𝑋 ∈ ( 𝑧 𝐿 𝑌 ) )
81 79 80 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → 𝑋 ∈ ( ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) ∖ ( 𝑧 𝐿 𝑌 ) ) )
82 1 2 3 4 48 55 63 81 plngcp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑤 ) = ( ( 𝑧 𝐿 𝑌 ) 𝐸 𝑋 ) )
83 47 82 78 3eqtr2rd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) ∧ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) ) ∧ 𝑤 ≠ 𝑧 ) → ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) )
84 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
85 84 25 37 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ≠ 𝑧 )
86 1 2 3 14 44 24 85 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑌 𝐿 𝑧 ) ∈ ran 𝐿 )
87 1 2 3 14 44 24 85 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑌 𝐿 𝑧 ) )
88 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑌 ∈ 𝐴 )
89 nelne1 ⊢ ( ( 𝑌 ∈ ( 𝑌 𝐿 𝑧 ) ∧ ¬ 𝑌 ∈ 𝐴 ) → ( 𝑌 𝐿 𝑧 ) ≠ 𝐴 )
90 87 88 89 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑌 𝐿 𝑧 ) ≠ 𝐴 )
91 90 necomd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → 𝐴 ≠ ( 𝑌 𝐿 𝑧 ) )
92 1 2 3 14 22 86 23 91 tglnpt4 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑤 ∈ ( 𝐴 ∖ ( 𝑌 𝐿 𝑧 ) ) 𝑤 ≠ 𝑧 )
93 83 92 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) )
94 27 93 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝐴 𝐸 𝑅 ) )
95 oveq2 ⊢ ( 𝑠 = 𝑧 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) )
96 95 eqeq2d ⊢ ( 𝑠 = 𝑧 → ( ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑧 ) ) )
97 96 26 93 rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) )
98 94 97 jca ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝐴 𝐸 𝑅 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
99 11 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = ( 𝑋 𝐿 𝑌 ) )
100 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
101 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝐴 ∈ ran 𝐿 )
102 15 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
103 17 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
104 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑌 )
105 1 2 3 100 102 103 104 tgelrnln ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
106 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) )
107 3 100 101 105 106 tglinesseq ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ) → 𝐴 = ( 𝑋 𝐿 𝑌 ) )
108 99 107 mtand ⊢ ( 𝜑 → ¬ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) )
109 nssrex ⊢ ( ¬ 𝐴 ⊆ ( 𝑋 𝐿 𝑌 ) ↔ ∃ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
110 108 109 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ ( 𝑋 𝐿 𝑌 ) )
111 98 110 r19.29a ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝐴 𝐸 𝑅 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝐴 𝐸 𝑅 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )