Metamath Proof Explorer

Theorem lnssplng

Description: A line defined by two points X and Y , both on a plane H , is entirely contained in H . Theorem 9.25 of Schwabhauser p. 75. (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 )
lnssplng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
lnssplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
lnssplng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
lnssplng.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
Assertion lnssplng ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ⊆ 𝐻 ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )

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 lnssplng.h ⊢ ( 𝜑 → 𝐻 ∈ ran 𝐸 )
7 lnssplng.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐻 )
8 lnssplng.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐻 )
9 lnssplng.1 ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
10 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑎 = ( 𝑋 𝐿 𝑌 ) )
11 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
12 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑎 ∈ ran 𝐿 )
13 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
14 1 2 3 4 11 12 13 elplnglnid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑎 ⊆ ( 𝑎 𝐸 𝑟 ) )
15 10 14 eqsstrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) )
16 oveq2 ⊢ ( 𝑠 = 𝑟 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑟 ) )
17 16 eqeq2d ⊢ ( 𝑠 = 𝑟 → ( ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑟 ) ) )
18 13 eldifad ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑟 ∈ 𝑃 )
19 13 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑟 ∈ 𝑎 )
20 19 10 neleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑟 ∈ ( 𝑋 𝐿 𝑌 ) )
21 18 20 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → 𝑟 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) )
22 10 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑟 ) )
23 17 21 22 rspcedvdw ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) )
24 15 23 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 = ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
25 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝐺 ∈ TarskiG )
26 25 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝐺 ∈ TarskiG )
27 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝐻 )
28 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝐻 = ( 𝑎 𝐸 𝑟 ) )
29 27 28 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ ( 𝑎 𝐸 𝑟 ) )
30 29 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑌 ∈ ( 𝑎 𝐸 𝑟 ) )
31 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝐻 )
32 31 28 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ ( 𝑎 𝐸 𝑟 ) )
33 32 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑋 ∈ ( 𝑎 𝐸 𝑟 ) )
34 9 necomd ⊢ ( 𝜑 → 𝑌 ≠ 𝑋 )
35 34 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑌 ≠ 𝑋 )
36 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑎 ∈ ran 𝐿 )
37 36 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑎 ∈ ran 𝐿 )
38 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
39 38 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
40 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) )
41 1 2 3 4 5 6 7 plngrnssp ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
42 1 2 3 4 5 6 8 plngrnssp ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
43 1 2 3 5 41 42 9 tglinecom ⊢ ( 𝜑 → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑋 ) )
44 43 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → ( 𝑋 𝐿 𝑌 ) = ( 𝑌 𝐿 𝑋 ) )
45 40 44 neeqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → 𝑎 ≠ ( 𝑌 𝐿 𝑋 ) )
46 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → ¬ 𝑋 ∈ 𝑎 )
47 1 2 3 4 26 30 33 35 37 39 45 46 lnssplnglem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → ( ( 𝑌 𝐿 𝑋 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) ) )
48 43 sseq1d ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ↔ ( 𝑌 𝐿 𝑋 ) ⊆ ( 𝑎 𝐸 𝑟 ) ) )
49 43 difeq2d ⊢ ( 𝜑 → ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) = ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) )
50 43 oveq1d ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) )
51 50 eqeq2d ⊢ ( 𝜑 → ( ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ( 𝑎 𝐸 𝑟 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) ) )
52 49 51 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) ) )
53 48 52 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) ↔ ( ( 𝑌 𝐿 𝑋 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) ) ) )
54 53 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → ( ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) ↔ ( ( 𝑌 𝐿 𝑋 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑌 𝐿 𝑋 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑌 𝐿 𝑋 ) 𝐸 𝑠 ) ) ) )
55 47 54 mpbird ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑋 ∈ 𝑎 ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
56 25 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝐺 ∈ TarskiG )
57 32 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑋 ∈ ( 𝑎 𝐸 𝑟 ) )
58 29 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑌 ∈ ( 𝑎 𝐸 𝑟 ) )
59 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ≠ 𝑌 )
60 59 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑋 ≠ 𝑌 )
61 36 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑎 ∈ ran 𝐿 )
62 38 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) )
63 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) )
64 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → ¬ 𝑌 ∈ 𝑎 )
65 1 2 3 4 56 57 58 60 61 62 63 64 lnssplnglem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ¬ 𝑌 ∈ 𝑎 ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
66 59 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → ¬ 𝑋 = 𝑌 )
67 25 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝐺 ∈ TarskiG )
68 36 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑎 ∈ ran 𝐿 )
69 1 2 3 4 25 36 38 32 plngssp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑋 ∈ 𝑃 )
70 1 2 3 4 25 36 38 29 plngssp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → 𝑌 ∈ 𝑃 )
71 1 2 3 25 69 70 59 tgelrnln ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
72 71 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → ( 𝑋 𝐿 𝑌 ) ∈ ran 𝐿 )
73 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) )
74 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 ∈ 𝑎 )
75 69 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 ∈ 𝑃 )
76 70 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑌 ∈ 𝑃 )
77 59 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 ≠ 𝑌 )
78 1 2 3 67 75 76 77 tglinerflx1 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑌 ) )
79 74 78 elind ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 ∈ ( 𝑎 ∩ ( 𝑋 𝐿 𝑌 ) ) )
80 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑌 ∈ 𝑎 )
81 1 2 3 67 75 76 77 tglinerflx2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑌 ∈ ( 𝑋 𝐿 𝑌 ) )
82 80 81 elind ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑌 ∈ ( 𝑎 ∩ ( 𝑋 𝐿 𝑌 ) ) )
83 1 2 3 67 68 72 73 79 82 tglineineq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ) → 𝑋 = 𝑌 )
84 66 83 mtand ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → ¬ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) )
85 ianor ⊢ ( ¬ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ) ↔ ( ¬ 𝑋 ∈ 𝑎 ∨ ¬ 𝑌 ∈ 𝑎 ) )
86 84 85 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → ( ¬ 𝑋 ∈ 𝑎 ∨ ¬ 𝑌 ∈ 𝑎 ) )
87 55 65 86 mpjaodan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) ∧ 𝑎 ≠ ( 𝑋 𝐿 𝑌 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
88 24 87 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
89 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → 𝐻 = ( 𝑎 𝐸 𝑟 ) )
90 89 sseq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ 𝐻 ↔ ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ) )
91 89 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
92 91 rexbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ↔ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
93 90 92 anbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( ( ( 𝑋 𝐿 𝑌 ) ⊆ 𝐻 ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) ↔ ( ( 𝑋 𝐿 𝑌 ) ⊆ ( 𝑎 𝐸 𝑟 ) ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) ( 𝑎 𝐸 𝑟 ) = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) ) )
94 88 93 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) ) ∧ 𝐻 = ( 𝑎 𝐸 𝑟 ) ) → ( ( 𝑋 𝐿 𝑌 ) ⊆ 𝐻 ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )
95 1 2 3 4 5 6 isplng ⊢ ( 𝜑 → ∃ 𝑎 ∈ ran 𝐿 ∃ 𝑟 ∈ ( 𝑃 ∖ 𝑎 ) 𝐻 = ( 𝑎 𝐸 𝑟 ) )
96 94 95 r19.29vva ⊢ ( 𝜑 → ( ( 𝑋 𝐿 𝑌 ) ⊆ 𝐻 ∧ ∃ 𝑠 ∈ ( 𝑃 ∖ ( 𝑋 𝐿 𝑌 ) ) 𝐻 = ( ( 𝑋 𝐿 𝑌 ) 𝐸 𝑠 ) ) )