plngrotlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plngrotlem2		Structured version Visualization version GIF version

Theorem plngrotlem2 29027

Description: Lemma for plngrot 29029. (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	⊢ (𝜑 → 𝑌 ≠ 𝑊)

**Assertion**
Ref	Expression
plngrotlem2	⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))

Distinct variable groups: 𝑡,𝐸 𝐺,𝑎,𝑏,𝑡 𝐼,𝑎,𝑏,𝑡 𝐿,𝑎,𝑏,𝑡 𝑂,𝑎,𝑏,𝑡 𝑃,𝑎,𝑏,𝑡 𝑊,𝑎,𝑏,𝑡 𝑋,𝑎,𝑏,𝑡 𝑌,𝑎,𝑏,𝑡 𝑍,𝑎,𝑏,𝑡 𝜑,𝑡 Allowed substitution hints: 𝜑(𝑎,𝑏) 𝐸(𝑎,𝑏)

Proof of Theorem plngrotlem2 Dummy variable 𝑠 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		plngval.p	. . . . 5 ⊢ 𝑃 = (Base‘𝐺)
2		plngval.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
3		plngval.1	. . . . 5 ⊢ 𝐿 = (LineG‘𝐺)
4		plngval.e	. . . . 5 ⊢ 𝐸 = (hlG‘𝐺)
5		plngval.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6	5	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝐺 ∈ TarskiG)
7		plngrot.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
8	7	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
9		plngrot.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
10	9	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑌 ∈ 𝑃)
11		plngrot.z	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
12	11	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
13		plngrot.1	. . . . . 6 ⊢ (𝜑 → 𝑋 ≠ 𝑌)
14	13	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑋 ≠ 𝑌)
15		plngrotlem2.4	. . . . 5 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ 𝑏 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) ∧ ∃𝑡 ∈ (𝑋𝐿𝑌)𝑡 ∈ (𝑎𝐼𝑏))}
16		plngrotlem2.1	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ 𝑃)
17	16	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑊 ∈ 𝑃)
18		plngrotlem2.2	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ (𝑍𝐼𝑊))
19	18	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑌 ∈ (𝑍𝐼𝑊))
20		plngrotlem2.3	. . . . . 6 ⊢ (𝜑 → 𝑌 ≠ 𝑊)
21	20	ad2antrr 738	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑌 ≠ 𝑊)
22		simpr 489	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
23	22	adantr 485	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍))
24		simpr 489	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍))
25	1, 2, 3, 4, 6, 8, 10, 12, 14, 15, 17, 19, 21, 23, 24	plngrotlem1 29026	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
26	5	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝐺 ∈ TarskiG)
27	7	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
28	11	eldifad 3925	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
29	28	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ∈ 𝑃)
30	9	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ∈ 𝑃)
31	7	eldifad 3925	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
32	1, 2, 3, 5, 31, 9, 13	tglinerflx2 28868	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
33		elndif 4095	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ (𝑋𝐿𝑌) → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
34	32, 33	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
35		nelne2 3062	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) → 𝑍 ≠ 𝑌)
36	11, 34, 35	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
37	36	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ≠ 𝑌)
38	1, 2, 3, 26, 29, 30, 37	tglinecom 28869	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑍𝐿𝑌) = (𝑌𝐿𝑍))
39	16	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑊 ∈ 𝑃)
40	20	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ≠ 𝑊)
41	1, 2, 3, 5, 9, 16, 28, 20, 18	btwnlng2 28854	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑊))
42	41	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ∈ (𝑌𝐿𝑊))
43	1, 2, 3, 26, 30, 39, 40, 29, 37, 42	tglineelsb2 28866	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑌𝐿𝑊) = (𝑌𝐿𝑍))
44	1, 2, 3, 26, 30, 39, 40	tglinecom 28869	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑌𝐿𝑊) = (𝑊𝐿𝑌))
45	38, 43, 44	3eqtr2d 2810	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑍𝐿𝑌) = (𝑊𝐿𝑌))
46	45	difeq2d 4089	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑃 ∖ (𝑍𝐿𝑌)) = (𝑃 ∖ (𝑊𝐿𝑌)))
47	27, 46	eleqtrd 2871	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ∈ (𝑃 ∖ (𝑊𝐿𝑌)))
48	20	neneqd 2969	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑌 = 𝑊)
49	5	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝐺 ∈ TarskiG)
50	31	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑋 ∈ 𝑃)
51	9	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ 𝑃)
52	13	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑋 ≠ 𝑌)
53	1, 2, 3, 49, 50, 51, 52	tgelrnln 28864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
54	28	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
55	36	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑌)
56	1, 2, 3, 49, 54, 51, 55	tgelrnln 28864	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
57	1, 2, 3, 5, 28, 9, 36	tglinerflx1 28867	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (𝑍𝐿𝑌))
58	57	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑌))
59	11	eldifbd 3926	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
60	59	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
61		nelne1 3061	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑍𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
62	58, 60, 61	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
63	62	necomd 3019	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ≠ (𝑍𝐿𝑌))
64	32	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
65	1, 2, 3, 49, 54, 51, 55	tglinerflx2 28868	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐿𝑌))
66	64, 65	elind 4161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
67		simpr 489	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑋𝐿𝑌))
68	16	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ 𝑃)
69	18	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐼𝑊))
70	1, 2, 3, 49, 54, 51, 68, 55, 69	btwnlng3 28855	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑍𝐿𝑌))
71	67, 70	elind 4161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
72	1, 2, 3, 49, 53, 56, 63, 66, 71	tglineineq 28877	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 = 𝑊)
73	48, 72	mtand 827	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
74	73	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
75	39, 74	eldifd 3924	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑊 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
76	13	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ≠ 𝑌)
77		eqid 2769	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
78	1, 77, 2, 5, 28, 9, 16, 18	tgbtwncom 28722	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑊𝐼𝑍))
79	78	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ∈ (𝑊𝐼𝑍))
80	37	necomd 3019	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ≠ 𝑍)
81	1, 77, 2, 15, 16, 28, 32, 73, 59, 78	islnoppd 28979	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑊𝑂𝑍)
82	81	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑊𝑂𝑍)
83	5	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝐺 ∈ TarskiG)
84	83	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝐺 ∈ TarskiG)
85	31	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑋 ∈ 𝑃)
86	9	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑌 ∈ 𝑃)
87	13	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑋 ≠ 𝑌)
88	1, 2, 3, 83, 85, 86, 87	tgelrnln 28864	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
89	88	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑋𝐿𝑌) ∈ ran 𝐿)
90	11	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
91	1, 2, 3, 4, 83, 88, 90, 22	plngssp 29020	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑠 ∈ 𝑃)
92	91	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑠 ∈ 𝑃)
93	16	ad3antrrr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑊 ∈ 𝑃)
94	28	ad3antrrr 742	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑍 ∈ 𝑃)
95		simpr 489	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑠𝑂𝑍)
96	1, 2, 3, 15, 84, 89, 92, 93, 94, 95	lnopp2hpgb 29003	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑊𝑂𝑍 ↔ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
97	82, 96	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)
98	97	orcd 886	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊))
99	98	ex 417	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) → (𝑠𝑂𝑍 → (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)))
100	99	ex 417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → (𝑠𝑂𝑍 → (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊))))
101	100	a2d 30	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → ((¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠𝑂𝑍) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊))))
102		df-or 861	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍) ↔ (¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠𝑂𝑍))
103		df-or 861	. . . . . . . . . 10 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)) ↔ (¬ 𝑠 ∈ (𝑋𝐿𝑌) → (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)))
104	101, 102, 103	3imtr4g 299	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊))))
105	104	imp 411	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)))
106		3orass 1104	. . . . . . . 8 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊) ↔ (𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)))
107	105, 106	sylibr 237	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊))
108	88	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
109	91	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ 𝑃)
110	1, 2, 3, 4, 26, 108, 75, 15, 109	elplng 29019	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑊) ↔ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊)))
111	107, 110	mpbird 260	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑊))
112	32	ad3antrrr 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑌 ∈ (𝑋𝐿𝑌))
113	59	ad3antrrr 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
114	73	ad3antrrr 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
115	18	ad3antrrr 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑌 ∈ (𝑍𝐼𝑊))
116	1, 77, 2, 15, 94, 93, 112, 113, 114, 115	islnoppd 28979	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑍𝑂𝑊)
117	1, 2, 3, 15, 84, 89, 94, 93, 116	lnoppnhpg 29004	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → ¬ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)
118	89	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → (𝑋𝐿𝑌) ∈ ran 𝐿)
119	84	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → 𝐺 ∈ TarskiG)
120	93	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → 𝑊 ∈ 𝑃)
121	92	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → 𝑠 ∈ 𝑃)
122		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → 𝑊𝑂𝑠)
123	1, 77, 2, 15, 3, 118, 119, 120, 121, 122	oppcom 28983	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑊𝑂𝑠) → 𝑠𝑂𝑊)
124	89	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → (𝑋𝐿𝑌) ∈ ran 𝐿)
125	84	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝐺 ∈ TarskiG)
126	92	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝑠 ∈ 𝑃)
127	93	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝑊 ∈ 𝑃)
128		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝑠𝑂𝑊)
129	1, 77, 2, 15, 3, 124, 125, 126, 127, 128	oppcom 28983	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝑊𝑂𝑠)
130	123, 129	impbida 812	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑊𝑂𝑠 ↔ 𝑠𝑂𝑊))
131	1, 77, 2, 15, 3, 89, 84, 92, 94, 95	oppcom 28983	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑍𝑂𝑠)
132	1, 2, 3, 15, 84, 89, 94, 93, 92, 131	lnopp2hpgb 29003	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑊𝑂𝑠 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
133	130, 132	bitr3d 284	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑠𝑂𝑊 ↔ 𝑍((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
134	117, 133	mtbird 328	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → ¬ 𝑠𝑂𝑊)
135	134	ex 417	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) → (𝑠𝑂𝑍 → ¬ 𝑠𝑂𝑊))
136	135	ex 417	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → (𝑠𝑂𝑍 → ¬ 𝑠𝑂𝑊)))
137	136	a2d 30	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → ((¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠𝑂𝑍) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → ¬ 𝑠𝑂𝑊)))
138	137	imp 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠𝑂𝑍)) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → ¬ 𝑠𝑂𝑊))
139	102, 138	sylan2b 605	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → ¬ 𝑠𝑂𝑊))
140	139	imp 411	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) → ¬ 𝑠𝑂𝑊)
141		df-3or 1102	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊) ↔ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊) ∨ 𝑠𝑂𝑊))
142		orcom 883	. . . . . . . . . . . . . . 15 ⊢ (((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊) ∨ 𝑠𝑂𝑊) ↔ (𝑠𝑂𝑊 ∨ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)))
143		df-or 861	. . . . . . . . . . . . . . 15 ⊢ ((𝑠𝑂𝑊 ∨ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)) ↔ (¬ 𝑠𝑂𝑊 → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)))
144	141, 142, 143	3bitri 300	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊 ∨ 𝑠𝑂𝑊) ↔ (¬ 𝑠𝑂𝑊 → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)))
145	107, 144	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (¬ 𝑠𝑂𝑊 → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)))
146	145	imp 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠𝑂𝑊) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
147		df-or 861	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊) ↔ (¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
148	146, 147	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠𝑂𝑊) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
149	148	imp 411	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠𝑂𝑊) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)
150	149	an32s 664	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ ¬ 𝑠𝑂𝑊) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)
151	140, 150	mpdan 699	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊)
152	151	ex 417	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (¬ 𝑠 ∈ (𝑋𝐿𝑌) → 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
153	152, 147	sylibr 237	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑊))
154	1, 2, 3, 4, 26, 47, 30, 75, 76, 15, 29, 79, 80, 111, 153	plngrotlem1 29026	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ ((𝑊𝐿𝑌)𝐸𝑋))
155	45	eqcomd 2775	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑊𝐿𝑌) = (𝑍𝐿𝑌))
156	155	oveq1d 7426	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → ((𝑊𝐿𝑌)𝐸𝑋) = ((𝑍𝐿𝑌)𝐸𝑋))
157	154, 156	eleqtrd 2871	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
158	1, 2, 3, 4, 83, 88, 90, 15, 91	elplng 29019	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍) ↔ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍)))
159	22, 158	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍))
160		3orass 1104	. . . . . 6 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍) ↔ (𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍)))
161		orordi 941	. . . . . 6 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ (𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍)) ↔ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍) ∨ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)))
162	160, 161	bitri 278	. . . . 5 ⊢ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍) ↔ ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍) ∨ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)))
163	159, 162	sylib 221	. . . 4 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → ((𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍) ∨ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)))
164	25, 157, 163	mpjaodan 973	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
165	164	ex 417	. 2 ⊢ (𝜑 → (𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋)))
166	165	ssrdv 3951	1 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 ∨ w3o 1100 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∃wrex 3095 ∖ cdif 3910 ⊆ wss 3913 class class class wbr 5113 {copab 5177 ran crn 5663 ‘cfv 6537 (class class class)co 7411 Basecbs 17268 distcds 17318 TarskiGcstrkg 28661 Itvcitv 28667 LineGclng 28668 hpGchpg 28997 hlGcplng 29012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 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 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-concat 14607 df-s1 14633 df-s2 14884 df-s3 14885 df-trkgc 28682 df-trkgb 28683 df-trkgcb 28684 df-trkgld 28686 df-trkg 28687 df-cgrg 28745 df-leg 28817 df-hlg 28835 df-mir 28891 df-rag 28932 df-perpg 28934 df-hpg 28998 df-plng 29013

This theorem is referenced by: plngrotlem3 29028

W3C validator