Theorem plngrotlem1 28991

Description: Lemma for plngrot 28994. (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 3916	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
8		plngrot.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
9		plngrot.x	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
10	9	eldifad 3916	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
11		plngrot.1	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
12	1, 2, 3, 5, 10, 8, 11	tglinerflx2 28800	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
13		elndif 4086	. . . . . . 7 ⊢ (𝑌 ∈ (𝑋𝐿𝑌) → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
14	12, 13	syl 17	. . . . . 6 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
15		nelne2 3055	. . . . . 6 ⊢ ((𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) → 𝑍 ≠ 𝑌)
16	6, 14, 15	syl2anc 593	. . . . 5 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
17	1, 2, 3, 5, 7, 8, 16	tgelrnln 28796	. . . 4 ⊢ (𝜑 → (𝑍𝐿𝑌) ∈ ran 𝐿)
18	1, 2, 3, 4, 5, 17, 9	elplnglnid 28987	. . 3 ⊢ (𝜑 → (𝑍𝐿𝑌) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
19	18	sselda 3936	. 2 ⊢ ((𝜑 ∧ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
20	5	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝐺 ∈ TarskiG)
21	20	ad2antrr 736	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝐺 ∈ TarskiG)
22	17	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
23	1, 2, 3, 5, 10, 8, 11	tgelrnln 28796	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋𝐿𝑌) ∈ ran 𝐿)
24		plngrotlem1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
25	1, 2, 3, 4, 5, 23, 6, 24	plngssp 28985	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ 𝑃)
26	25	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ 𝑃)
27		plngrotlem2.1	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
28	27	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ 𝑃)
29		simpr 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑆 = 𝑊)
30		plngrotlem2.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑊))
31	1, 2, 3, 5, 7, 8, 27, 16, 30	btwnlng3 28787	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ∈ (𝑍𝐿𝑌))
32	31	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑊 ∈ (𝑍𝐿𝑌))
33	29, 32	eqeltrd 2862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑆 = 𝑊) → 𝑆 ∈ (𝑍𝐿𝑌))
34	33	stoic1a 1792	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑆 = 𝑊)
35	34	neqned 2964	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ≠ 𝑊)
36	1, 2, 3, 20, 26, 28, 35	tgelrnln 28796	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝐿𝑊) ∈ ran 𝐿)
37	36	ad2antrr 736	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ∈ ran 𝐿)
38	26	ad2antrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ 𝑃)
39	28	ad2antrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ 𝑃)
40	23	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
41	40	ad2antrr 736	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
42		simplr 778	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑋𝐿𝑌))
43	1, 3, 2, 21, 41, 42	tglnpt 28715	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ 𝑃)
44	35	ad2antrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ≠ 𝑊)
45		eqid 2762	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
46		simpr 488	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑊𝐼𝑆))
47	1, 45, 2, 21, 39, 43, 38, 46	tgbtwncom 28654	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑆𝐼𝑊))
48	1, 2, 3, 21, 38, 39, 43, 44, 47	btwnlng1 28785	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (𝑆𝐿𝑊))
49		plngrotlem2.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ≠ 𝑊)
50	49	neneqd 2962	. . . . . . . . . 10 ⊢ (𝜑 → ¬ 𝑌 = 𝑊)
51	50	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑌 = 𝑊)
52	5	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
53	23	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
54	17	ad2antrr 736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
55	7	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ 𝑃)
56	8	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ 𝑃)
57	16	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑌)
58	1, 2, 3, 20, 55, 56, 57	tglinerflx1 28799	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑌))
59	6	eldifbd 3917	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
60	59	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
61		nelne1 3054	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑍𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
62	58, 60, 61	syl2an2r 695	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
63	62	necomd 3012	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ≠ (𝑍𝐿𝑌))
64	12	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
65	7	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
66	8	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ 𝑃)
67	16	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑌)
68	1, 2, 3, 52, 65, 66, 67	tglinerflx2 28800	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐿𝑌))
69	64, 68	elind 4152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
70		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑋𝐿𝑌))
71	27	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
72	30	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐼𝑊))
73	1, 2, 3, 52, 65, 66, 71, 67, 72	btwnlng3 28787	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑍𝐿𝑌))
74	70, 73	elind 4152	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
75	1, 2, 3, 52, 53, 54, 63, 69, 74	tglineineq 28809	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 = 𝑊)
76	51, 75	mtand 825	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
77	76	ad2antrr 736	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
78		nelne2 3055	. . . . . . 7 ⊢ ((𝑡 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑡 ≠ 𝑊)
79	42, 77, 78	syl2anc 593	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ≠ 𝑊)
80	1, 2, 3, 21, 38, 39, 44	tglinerflx1 28799	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ (𝑆𝐿𝑊))
81		simpllr 785	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑆 ∈ (𝑍𝐿𝑌))
82		nelne1 3054	. . . . . . . . 9 ⊢ ((𝑆 ∈ (𝑆𝐿𝑊) ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝐿𝑊) ≠ (𝑍𝐿𝑌))
83	80, 81, 82	syl2anc 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ≠ (𝑍𝐿𝑌))
84	83	necomd 3012	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ≠ (𝑆𝐿𝑊))
85	31	ad3antrrr 740	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ (𝑍𝐿𝑌))
86	1, 2, 3, 21, 38, 39, 44	tglinerflx2 28800	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ (𝑆𝐿𝑊))
87	85, 86	elind 4152	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ∈ ((𝑍𝐿𝑌) ∩ (𝑆𝐿𝑊)))
88	1, 2, 3, 21, 22, 37, 84, 87	tglineinsn 28810	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌) ∩ (𝑆𝐿𝑊)) = {𝑊})
89	1, 2, 3, 4, 21, 22, 37, 48, 39, 79, 88	lnincplng 28988	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ⊆ ((𝑍𝐿𝑌)𝐸𝑡))
90	9	ad3antrrr 740	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
91	10	ad3antrrr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ 𝑃)
92	56	ad2antrr 736	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ 𝑃)
93	11	ad3antrrr 740	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ≠ 𝑌)
94	1, 2, 3, 21, 91, 92, 93	tglinerflx1 28799	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑋 ∈ (𝑋𝐿𝑌))
95	58	ad2antrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ∈ (𝑍𝐿𝑌))
96	59	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
97	96	ad2antrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
98	95, 97, 61	syl2anc 593	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
99	55	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ∈ 𝑃)
100	57	ad2antrr 736	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑍 ≠ 𝑌)
101	1, 2, 3, 21, 99, 92, 100	tglinerflx2 28800	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ (𝑍𝐿𝑌))
102	12	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
103	102	ad2antrr 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ (𝑋𝐿𝑌))
104	101, 103	elind 4152	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑌 ∈ ((𝑍𝐿𝑌) ∩ (𝑋𝐿𝑌)))
105	1, 2, 3, 21, 22, 41, 98, 104	tglineinsn 28810	. . . . . . . . 9 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌) ∩ (𝑋𝐿𝑌)) = {𝑌})
106	1, 2, 3, 4, 21, 22, 41, 94, 92, 93, 105	lnincplng 28988	. . . . . . . 8 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑋𝐿𝑌) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
107	106, 42	sseldd 3937	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
108	21	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝐺 ∈ TarskiG)
109	43	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ 𝑃)
110	39	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ 𝑃)
111	38	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ 𝑃)
112	79	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ≠ 𝑊)
113	47	adantr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑆𝐼𝑊))
114	1, 2, 3, 108, 109, 110, 111, 112, 113	btwnlng2 28786	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ (𝑡𝐿𝑊))
115	55	ad3antrrr 740	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ∈ 𝑃)
116	97	adantr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
117		nelne2 3055	. . . . . . . . . . . . 13 ⊢ ((𝑡 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → 𝑡 ≠ 𝑍)
118	42, 116, 117	syl2an2r 695	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ≠ 𝑍)
119	118	necomd 3012	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑡)
120	1, 2, 3, 108, 115, 109, 119	tglinecom 28801	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑡) = (𝑡𝐿𝑍))
121	16	necomd 3012	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑌 ≠ 𝑍)
122	1, 45, 2, 5, 7, 8, 27, 30, 121	tgbtwnne 28656	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ≠ 𝑊)
123	122	ad4antr 742	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑍 ≠ 𝑊)
124		simpr 488	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑍𝐿𝑌))
125	1, 2, 3, 5, 7, 27, 8, 122, 30	btwnlng1 28785	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐿𝑊))
126	1, 2, 3, 5, 7, 27, 122, 8, 121, 125	tglineelsb2 28798	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑍𝐿𝑊) = (𝑍𝐿𝑌))
127	126	ad4antr 742	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑊) = (𝑍𝐿𝑌))
128	124, 127	eleqtrrd 2865	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑡 ∈ (𝑍𝐿𝑊))
129	1, 2, 3, 108, 115, 110, 123, 109, 118, 128	tglineelsb2 28798	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑊) = (𝑍𝐿𝑡))
130	129, 127	eqtr3d 2799	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑍𝐿𝑡) = (𝑍𝐿𝑌))
131	79	necomd 3012	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑊 ≠ 𝑡)
132	131	adantr 484	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ≠ 𝑡)
133	1, 2, 3, 108, 109, 115, 110, 118, 128, 123	lnrot2 28790	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑊 ∈ (𝑡𝐿𝑍))
134	1, 2, 3, 108, 109, 115, 118, 110, 132, 133	tglineelsb2 28798	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑡𝐿𝑍) = (𝑡𝐿𝑊))
135	120, 130, 134	3eqtr3rd 2806	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → (𝑡𝐿𝑊) = (𝑍𝐿𝑌))
136	114, 135	eleqtrd 2864	. . . . . . . 8 ⊢ (((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) ∧ 𝑡 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ (𝑍𝐿𝑌))
137	81, 136	mtand 825	. . . . . . 7 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ¬ 𝑡 ∈ (𝑍𝐿𝑌))
138	107, 137	eldifd 3915	. . . . . 6 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑡 ∈ (((𝑍𝐿𝑌)𝐸𝑋) ∖ (𝑍𝐿𝑌)))
139	1, 2, 3, 4, 21, 22, 90, 138	plngcp 28990	. . . . 5 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → ((𝑍𝐿𝑌)𝐸𝑋) = ((𝑍𝐿𝑌)𝐸𝑡))
140	89, 139	sseqtrrd 3973	. . . 4 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → (𝑆𝐿𝑊) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))
141	140, 80	sseldd 3937	. . 3 ⊢ ((((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑡 ∈ (𝑋𝐿𝑌)) ∧ 𝑡 ∈ (𝑊𝐼𝑆)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
142		eleq1 2850	. . . . 5 ⊢ (𝑡 = 𝑆 → (𝑡 ∈ (𝑊𝐼𝑆) ↔ 𝑆 ∈ (𝑊𝐼𝑆)))
143		simpr 488	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ (𝑋𝐿𝑌))
144	5	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
145	27	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
146	25	ad2antrr 736	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ 𝑃)
147	1, 45, 2, 144, 145, 146	tgbtwntriv2 28653	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ (𝑊𝐼𝑆))
148	142, 143, 147	rspcedvdw 3584	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ 𝑆 ∈ (𝑋𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
149		plngrotlem2.4	. . . . . . 7 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑎𝐼𝑏))}
150	23	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
151	5	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
152	25	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆 ∈ 𝑃)
153	27	ad2antrr 736	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
154	7	ad2antrr 736	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
155		plngrotlem1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∈ (𝑋𝐿𝑌) ∨ 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
156	155	ord 875	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ 𝑆 ∈ (𝑋𝐿𝑌) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
157	156	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (¬ 𝑆 ∈ (𝑋𝐿𝑌) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
158	157	imp 410	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)
159	1, 2, 3, 151, 150, 152, 149, 154, 158	hpgcom 28937	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆)
160	30	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑌 ∈ (𝑍𝐼𝑊))
161	1, 45, 2, 149, 55, 28, 102, 96, 76, 160	islnoppd 28910	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑍𝑂𝑊)
162	1, 2, 3, 149, 20, 40, 55, 26, 28, 161	lnopp2hpgb 28933	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆𝑂𝑊 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆))
163	162	adantr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑆𝑂𝑊 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑆))
164	159, 163	mpbird 259	. . . . . . 7 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑆𝑂𝑊)
165	1, 45, 2, 149, 3, 150, 151, 152, 153, 164	oppcom 28914	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → 𝑊𝑂𝑆)
166	1, 45, 2, 149, 153, 152	islnopp 28909	. . . . . 6 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → (𝑊𝑂𝑆 ↔ ((¬ 𝑊 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))))
167	165, 166	mpbid 234	. . . . 5 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → ((¬ 𝑊 ∈ (𝑋𝐿𝑌) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆)))
168	167	simprd 499	. . . 4 ⊢ (((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) ∧ ¬ 𝑆 ∈ (𝑋𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
169		exmidd 906	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → (𝑆 ∈ (𝑋𝐿𝑌) ∨ ¬ 𝑆 ∈ (𝑋𝐿𝑌)))
170	148, 168, 169	mpjaodan 971	. . 3 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑊𝐼𝑆))
171	141, 170	r19.29a 3170	. 2 ⊢ ((𝜑 ∧ ¬ 𝑆 ∈ (𝑍𝐿𝑌)) → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
172		exmidd 906	. 2 ⊢ (𝜑 → (𝑆 ∈ (𝑍𝐿𝑌) ∨ ¬ 𝑆 ∈ (𝑍𝐿𝑌)))
173	19, 171, 172	mpjaodan 971	1 ⊢ (𝜑 → 𝑆 ∈ ((𝑍𝐿𝑌)𝐸𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∃wrex 3086   ∖ cdif 3901   class class class wbr 5100  {copab 5162  ran crn 5648  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  distcds 17295  TarskiGcstrkg 28593  Itvcitv 28599  LineGclng 28600  hpGchpg 28927  hlGcplng 28977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-om 7847  df-1st 7970  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-oadd 8441  df-er 8678  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-dju 9859  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-2 12280  df-3 12281  df-n0 12482  df-xnn0 12555  df-z 12569  df-uz 12840  df-fz 13513  df-fzo 13660  df-hash 14344  df-word 14527  df-concat 14584  df-s1 14610  df-s2 14861  df-s3 14862  df-trkgc 28614  df-trkgb 28615  df-trkgcb 28616  df-trkgld 28618  df-trkg 28619  df-cgrg 28677  df-leg 28749  df-hlg 28767  df-mir 28823  df-rag 28864  df-perpg 28866  df-hpg 28928  df-plng 28978

This theorem is referenced by:  plngrotlem2  28992