Theorem plngrotlem1 29258

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

Hypotheses

Ref	Expression
plngval.p	⊢ 𝑃 = (Base‘𝐺)
plngval.i	⊢ 𝐼 = (Itv‘𝐺)
plngval.1	⊢ 𝐿 = (LineG‘𝐺)
plngval.e	⊢ 𝐸 = (hlG‘𝐺)
plngval.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
plngrot.x	⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
plngrot.y	⊢ (𝜑 → 𝑌 ∈ 𝑃)
plngrot.z	⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
plngrot.1	⊢ (𝜑 → 𝑋 ≠ 𝑌)
plngrotlem2.4	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑎𝐼𝑏))}
plngrotlem2.1	⊢ (𝜑 → 𝑊 ∈ 𝑃)
plngrotlem2.2	⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑊))
plngrotlem2.3	⊢ (𝜑 → 𝑌 ≠ 𝑊)
plngrotlem1.1	⊢ (𝜑 → 𝑆 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
plngrotlem1.2	⊢ (𝜑 → (𝑆 ∈ (𝑋𝐿𝑌) ∨ 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))

Assertion

Ref	Expression
plngrotlem1	⊢ (𝜑 → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))

Distinct variable groups:   𝑡,𝐸   𝐺,𝑎,𝑏,𝑡   𝐼,𝑎,𝑏,𝑡   𝐿,𝑎,𝑏,𝑡   𝑂,𝑎,𝑏,𝑡   𝑃,𝑎,𝑏,𝑡   𝑡,𝑆   𝑊,𝑎,𝑏,𝑡   𝑋,𝑎,𝑏,𝑡   𝑌,𝑎,𝑏,𝑡   𝑍,𝑎,𝑏,𝑡   𝜑,𝑡

Allowed substitution hints:   𝜑(𝑎, 𝑏)   𝑆(𝑎, 𝑏)   𝐸(𝑎, 𝑏)

Proof of Theorem plngrotlem1

Step	Hyp	Ref	Expression
1		plngval.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		plngval.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
3		plngval.1	. . . 4 ⊢ 𝐿 = (LineG‘𝐺)
4		plngval.e	. . . 4 ⊢ 𝐸 = (hlG‘𝐺)
5		plngval.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6		plngrot.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
7	6	eldifad 3911	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
8		plngrot.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
9		plngrot.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
10	9	eldifad 3911	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
11		plngrot.1	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
12	1, 2, 3, 5, 10, 8, 11	tglinerflx2 29095	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
13		elndif 4080	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋𝐿𝑌) → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
14	12, 13	syl 18	. . . . . 6 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
15		nelne2 3054	. . . . . 6 ⊢ ((𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) → 𝑍 ≠ 𝑌)
16	6, 14, 15	syl2anc 596	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
17	1, 2, 3, 5, 7, 8, 16	tgelrnln 29091	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑌) ∈ ran 𝐿)
18	1, 2, 3, 4, 5, 17, 9	elplnglnid 29254	. . 3 ⊢ (𝜑 → (𝑍𝐿𝑌) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
19	18	sselda 3931	. 2 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
20	5	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝐺 ∈ TarskiG)
21	20	ad2antrr 739	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝐺 ∈ TarskiG)
22	17	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
23	1, 2, 3, 5, 10, 8, 11	tgelrnln 29091	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
24		plngrotlem1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
25	1, 2, 3, 4, 5, 23, 6, 24	plngssp 29252	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
26	25	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ 𝑃)
27		plngrotlem2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
28	27	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ 𝑃)
29		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑆 = 𝑊)
30		plngrotlem2.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑊))
31	1, 2, 3, 5, 7, 8, 27, 16, 30	btwnlng3 29082	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑌))
32	31	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑊 ∈ (𝑍𝐿𝑌))
33	29, 32	eqeltrd 2861	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑆 ∈ (𝑍𝐿𝑌))
34	33	stoic1a 1805	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑆 = 𝑊)
35	34	neqned 2963	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ≠ 𝑊)
36	1, 2, 3, 20, 26, 28, 35	tgelrnln 29091	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝐿𝑊) ∈ ran 𝐿)
37	36	ad2antrr 739	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ∈ ran 𝐿)
38	26	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ 𝑃)
39	28	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ 𝑃)
40	23	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
41	40	ad2antrr 739	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
42		simplr 781	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑋𝐿𝑌))
43	1, 3, 2, 21, 41, 42	tglnpt 29005	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ 𝑃)
44	35	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ≠ 𝑊)
45		eqid 2761	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
46		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑊𝐼𝑆))
47	1, 45, 2, 21, 39, 43, 38, 46	tgbtwncom 28944	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑆𝐼𝑊))
48	1, 2, 3, 21, 38, 39, 43, 44, 47	btwnlng1 29080	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑆𝐿𝑊))
49		plngrotlem2.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑊)
50	49	neneqd 2961	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝑌 = 𝑊)
51	50	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑌 = 𝑊)
52	5	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
53	23	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
54	17	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
55	7	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ 𝑃)
56	8	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ 𝑃)
57	16	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑌)
58	1, 2, 3, 20, 55, 56, 57	tglinerflx1 29094	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑌))
59	6	eldifbd 3912	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
60	59	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
61		nelne1 3053	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑍𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
62	58, 60, 61	syl2an2r 698	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
63	62	necomd 3011	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ≠ (𝑍𝐿𝑌))
64	12	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
65	7	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
66	8	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ 𝑃)
67	16	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑌)
68	1, 2, 3, 52, 65, 66, 67	tglinerflx2 29095	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐿𝑌))
69	64, 68	elind 4146	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
70		simpr 490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑋𝐿𝑌))
71	27	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
72	30	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐼𝑊))
73	1, 2, 3, 52, 65, 66, 71, 67, 72	btwnlng3 29082	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑍𝐿𝑌))
74	70, 73	elind 4146	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
75	1, 2, 3, 52, 53, 54, 63, 69, 74	tglineineq 29104	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 = 𝑊)
76	51, 75	mtand 828	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
77	76	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
78		nelne2 3054	. . . . . . 7 ⊢ ((𝑡 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑡 ≠ 𝑊)
79	42, 77, 78	syl2anc 596	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ≠ 𝑊)
80	1, 2, 3, 21, 38, 39, 44	tglinerflx1 29094	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ (𝑆𝐿𝑊))
81		simpllr 788	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑆 ∈ (𝑍𝐿𝑌))
82		nelne1 3053	. . . . . . . . 9 ⊢ ((𝑆 ∈ (𝑆𝐿𝑊) ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝐿𝑊) ≠ (𝑍𝐿𝑌))
83	80, 81, 82	syl2anc 596	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ≠ (𝑍𝐿𝑌))
84	83	necomd 3011	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ≠ (𝑆𝐿𝑊))
85	31	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ (𝑍𝐿𝑌))
86	1, 2, 3, 21, 38, 39, 44	tglinerflx2 29095	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ (𝑆𝐿𝑊))
87	85, 86	elind 4146	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ ((𝑍𝐿𝑌) ∩ (𝑆𝐿𝑊)))
88	1, 2, 3, 21, 22, 37, 84, 87	tglineinsn 29105	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌) ∩ (𝑆𝐿𝑊)) = {𝑊})
89	1, 2, 3, 4, 21, 22, 37, 48, 39, 79, 88	lnincplng 29255	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ⊆ ((𝑍𝐿𝑌)𝐸𝑡))
90	9	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
91	10	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ 𝑃)
92	56	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ 𝑃)
93	11	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ≠ 𝑌)
94	1, 2, 3, 21, 91, 92, 93	tglinerflx1 29094	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ (𝑋𝐿𝑌))
95	58	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ∈ (𝑍𝐿𝑌))
96	59	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
97	96	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
98	95, 97, 61	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
99	55	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ∈ 𝑃)
100	57	ad2antrr 739	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ≠ 𝑌)
101	1, 2, 3, 21, 99, 92, 100	tglinerflx2 29095	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ (𝑍𝐿𝑌))
102	12	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
103	102	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ (𝑋𝐿𝑌))
104	101, 103	elind 4146	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ ((𝑍𝐿𝑌) ∩ (𝑋𝐿𝑌)))
105	1, 2, 3, 21, 22, 41, 98, 104	tglineinsn 29105	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌) ∩ (𝑋𝐿𝑌)) = {𝑌})
106	1, 2, 3, 4, 21, 22, 41, 94, 92, 93, 105	lnincplng 29255	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑋𝐿𝑌) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
107	106, 42	sseldd 3932	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
108	21	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝐺 ∈ TarskiG)
109	43	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ 𝑃)
110	39	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ 𝑃)
111	38	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ 𝑃)
112	79	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ≠ 𝑊)
113	47	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑆𝐼𝑊))
114	1, 2, 3, 108, 109, 110, 111, 112, 113	btwnlng2 29081	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ (𝑡𝐿𝑊))
115	55	ad3antrrr 743	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ 𝑃)
116	97	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
117		nelne2 3054	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑡 ≠ 𝑍)
118	42, 116, 117	syl2an2r 698	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ≠ 𝑍)
119	118	necomd 3011	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑡)
120	1, 2, 3, 108, 115, 109, 119	tglinecom 29096	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑡) = (𝑡𝐿𝑍))
121	16	necomd 3011	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
122	1, 45, 2, 5, 7, 8, 27, 30, 121	tgbtwnne 28946	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
123	122	ad4antr 745	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑊)
124		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑍𝐿𝑌))
125	1, 2, 3, 5, 7, 27, 8, 122, 30	btwnlng1 29080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐿𝑊))
126	1, 2, 3, 5, 7, 27, 122, 8, 121, 125	tglineelsb2 29093	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍𝐿𝑊) = (𝑍𝐿𝑌))
127	126	ad4antr 745	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑊) = (𝑍𝐿𝑌))
128	124, 127	eleqtrrd 2864	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑍𝐿𝑊))
129	1, 2, 3, 108, 115, 110, 123, 109, 118, 128	tglineelsb2 29093	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑊) = (𝑍𝐿𝑡))
130	129, 127	eqtr3d 2798	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑡) = (𝑍𝐿𝑌))
131	79	necomd 3011	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ≠ 𝑡)
132	131	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ≠ 𝑡)
133	1, 2, 3, 108, 109, 115, 110, 118, 128, 123	lnrot2 29085	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ (𝑡𝐿𝑍))
134	1, 2, 3, 108, 109, 115, 118, 110, 132, 133	tglineelsb2 29093	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑡𝐿𝑍) = (𝑡𝐿𝑊))
135	120, 130, 134	3eqtr3rd 2805	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑡𝐿𝑊) = (𝑍𝐿𝑌))
136	114, 135	eleqtrd 2863	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ (𝑍𝐿𝑌))
137	81, 136	mtand 828	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑡 ∈ (𝑍𝐿𝑌))
138	107, 137	eldifd 3910	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (((𝑍𝐿𝑌)𝐸𝑋) ∖ (𝑍𝐿𝑌)))
139	1, 2, 3, 4, 21, 22, 90, 138	plngcp 29257	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌)𝐸𝑋) = ((𝑍𝐿𝑌)𝐸𝑡))
140	89, 139	sseqtrrd 3968	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
141	140, 80	sseldd 3932	. . 3 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
142		eleq1 2849	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝑊𝐼𝑆) ↔ 𝑆 ∈ (𝑊𝐼𝑆)))
143		simpr 490	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ (𝑋𝐿𝑌))
144	5	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
145	27	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
146	25	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ 𝑃)
147	1, 45, 2, 144, 145, 146	tgbtwntriv2 28943	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ (𝑊𝐼𝑆))
148	142, 143, 147	rspcedvdw 3580	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
149		plngrotlem2.4	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑎𝐼𝑏))}
150	23	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
151	5	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
152	25	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ 𝑃)
153	27	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
154	7	ad2antrr 739	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
155		plngrotlem1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ (𝑋𝐿𝑌) ∨ 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
156	155	ord 878	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝑆 ∈ (𝑋𝐿𝑌) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
157	156	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (¬ 𝑆 ∈ (𝑋𝐿𝑌) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
158	157	imp 412	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)
159	1, 2, 3, 151, 150, 152, 149, 154, 158	hpgcom 29238	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆)
160	30	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ (𝑍𝐼𝑊))
161	1, 45, 2, 149, 55, 28, 102, 96, 76, 160	islnoppd 29209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍𝑂𝑊)
162	1, 2, 3, 149, 20, 40, 55, 26, 28, 161	lnopp2hpgb 29234	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝑂𝑊 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆))
163	162	adantr 486	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑆𝑂𝑊 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆))
164	159, 163	mpbird 260	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆𝑂𝑊)
165	1, 45, 2, 149, 3, 150, 151, 152, 153, 164	oppcom 29213	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊𝑂𝑆)
166	1, 45, 2, 149, 153, 152	islnopp 29208	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑊𝑂𝑆 ↔ ((¬ 𝑊 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))))
167	165, 166	mpbid 235	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → ((¬ 𝑊 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆)))
168	167	simprd 501	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
169		exmidd 909	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆 ∈ (𝑋𝐿𝑌) ∨ ¬ 𝑆 ∈ (𝑋𝐿𝑌)))
170	148, 168, 169	mpjaodan 973	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
171	141, 170	r19.29a 3171	. 2 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
172		exmidd 909	. 2 ⊢ (𝜑 → (𝑆 ∈ (𝑍𝐿𝑌) ∨ ¬ 𝑆 ∈ (𝑍𝐿𝑌)))
173	19, 171, 172	mpjaodan 973	1 ⊢ (𝜑 → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087   ∖ cdif 3896   class class class wbr 5103  {copab 5167  ran crn 5652  ‘cfv 6537  (class class class)co 7418  Basecbs 17380  distcds 17430  TarskiGcstrkg 28882  Itvcitv 28888  LineGclng 28889  hpGchpg 29228  hlGcplng 29244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-oadd 8473  df-er 8710  df-map 8842  df-pm 8843  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-dju 9975  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329  df-2 12398  df-3 12399  df-n0 12600  df-xnn0 12673  df-z 12687  df-uz 12959  df-fz 13633  df-fzo 13782  df-hash 14468  df-word 14652  df-concat 14709  df-s1 14736  df-s2 14992  df-s3 14993  df-trkgc 28903  df-trkgb 28904  df-trkgcb 28905  df-trkgld 28907  df-trkg 28908  df-cgrg 28967  df-leg 29039  df-hlg 29057  df-mir 29118  df-rag 29162  df-perpg 29164  df-hpg 29229  df-plng 29245

This theorem is used by:  plngrotlem2  29259