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 29070

Description: Lemma for plngrot 29072. (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 29069	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍)) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
26	5	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝐺 ∈ TarskiG)
27	7	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ∈ (𝑃 ∖ (𝑍𝐿𝑌)))
28	11	eldifad 3917	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
29	28	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ∈ 𝑃)
30	9	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ∈ 𝑃)
31	7	eldifad 3917	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
32	1, 2, 3, 5, 31, 9, 13	tglinerflx2 28907	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ (𝑋𝐿𝑌))
33		elndif 4087	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ (𝑋𝐿𝑌) → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
34	32, 33	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
35		nelne2 3056	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)) ∧ ¬ 𝑌 ∈ (𝑃 ∖ (𝑋𝐿𝑌))) → 𝑍 ≠ 𝑌)
36	11, 34, 35	syl2anc 595	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ≠ 𝑌)
37	36	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ≠ 𝑌)
38	1, 2, 3, 26, 29, 30, 37	tglinecom 28908	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑍𝐿𝑌) = (𝑌𝐿𝑍))
39	16	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑊 ∈ 𝑃)
40	20	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ≠ 𝑊)
41	1, 2, 3, 5, 9, 16, 28, 20, 18	btwnlng2 28893	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑍 ∈ (𝑌𝐿𝑊))
42	41	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑍 ∈ (𝑌𝐿𝑊))
43	1, 2, 3, 26, 30, 39, 40, 29, 37, 42	tglineelsb2 28905	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑌𝐿𝑊) = (𝑌𝐿𝑍))
44	1, 2, 3, 26, 30, 39, 40	tglinecom 28908	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑌𝐿𝑊) = (𝑊𝐿𝑌))
45	38, 43, 44	3eqtr2d 2804	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑍𝐿𝑌) = (𝑊𝐿𝑌))
46	45	difeq2d 4081	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑃 ∖ (𝑍𝐿𝑌)) = (𝑃 ∖ (𝑊𝐿𝑌)))
47	27, 46	eleqtrd 2865	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ∈ (𝑃 ∖ (𝑊𝐿𝑌)))
48	20	neneqd 2963	. . . . . . . . 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 28903	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
54	28	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ 𝑃)
55	36	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ≠ 𝑌)
56	1, 2, 3, 49, 54, 51, 55	tgelrnln 28903	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ∈ ran 𝐿)
57	1, 2, 3, 5, 28, 9, 36	tglinerflx1 28906	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑍 ∈ (𝑍𝐿𝑌))
58	57	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑍 ∈ (𝑍𝐿𝑌))
59	11	eldifbd 3918	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
60	59	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → ¬ 𝑍 ∈ (𝑋𝐿𝑌))
61		nelne1 3055	. . . . . . . . . . . 12 ⊢ ((𝑍 ∈ (𝑍𝐿𝑌) ∧ ¬ 𝑍 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
62	58, 60, 61	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑍𝐿𝑌) ≠ (𝑋𝐿𝑌))
63	62	necomd 3013	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → (𝑋𝐿𝑌) ≠ (𝑍𝐿𝑌))
64	32	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑋𝐿𝑌))
65	1, 2, 3, 49, 54, 51, 55	tglinerflx2 28907	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 ∈ (𝑍𝐿𝑌))
66	64, 65	elind 4153	. . . . . . . . . 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 28894	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ (𝑍𝐿𝑌))
71	67, 70	elind 4153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑊 ∈ ((𝑋𝐿𝑌) ∩ (𝑍𝐿𝑌)))
72	1, 2, 3, 49, 53, 56, 63, 66, 71	tglineineq 28916	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑊 ∈ (𝑋𝐿𝑌)) → 𝑌 = 𝑊)
73	48, 72	mtand 827	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
74	73	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → ¬ 𝑊 ∈ (𝑋𝐿𝑌))
75	39, 74	eldifd 3916	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑊 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
76	13	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑋 ≠ 𝑌)
77		eqid 2763	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
78	1, 77, 2, 5, 28, 9, 16, 18	tgbtwncom 28757	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ (𝑊𝐼𝑍))
79	78	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ∈ (𝑊𝐼𝑍))
80	37	necomd 3013	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑌 ≠ 𝑍)
81	1, 77, 2, 15, 16, 28, 32, 73, 59, 78	islnoppd 29021	. . . . . . . . . . . . . . . 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 28903	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑋𝐿𝑌) ∈ ran 𝐿)
89	88	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑋𝐿𝑌) ∈ ran 𝐿)
90	11	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → 𝑍 ∈ (𝑃 ∖ (𝑋𝐿𝑌)))
91	1, 2, 3, 4, 83, 88, 90, 22	plngssp 29063	. . . . . . . . . . . . . . . . 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 29045	. . . . . . . . . . . . . . 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 1106	. . . . . . . 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 29062	. . . . . . 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 29021	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑍𝑂𝑊)
117	1, 2, 3, 15, 84, 89, 94, 93, 116	lnoppnhpg 29046	. . . . . . . . . . . . . . . 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 29025	. . . . . . . . . . . . . . . . . 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 29025	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) ∧ 𝑠𝑂𝑊) → 𝑊𝑂𝑠)
130	123, 129	impbida 812	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → (𝑊𝑂𝑠 ↔ 𝑠𝑂𝑊))
131	1, 77, 2, 15, 3, 89, 84, 92, 94, 95	oppcom 29025	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ ¬ 𝑠 ∈ (𝑋𝐿𝑌)) ∧ 𝑠𝑂𝑍) → 𝑍𝑂𝑠)
132	1, 2, 3, 15, 84, 89, 94, 93, 92, 131	lnopp2hpgb 29045	. . . . . . . . . . . . . . . . 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 1104	. . . . . . . . . . . . . . 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 29069	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ ((𝑊𝐿𝑌)𝐸𝑋))
155	45	eqcomd 2769	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → (𝑊𝐿𝑌) = (𝑍𝐿𝑌))
156	155	oveq1d 7425	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → ((𝑊𝐿𝑌)𝐸𝑋) = ((𝑍𝐿𝑌)𝐸𝑋))
157	154, 156	eleqtrd 2865	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) ∧ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠𝑂𝑍)) → 𝑠 ∈ ((𝑍𝐿𝑌)𝐸𝑋))
158	1, 2, 3, 4, 83, 88, 90, 15, 91	elplng 29062	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍) ↔ (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍)))
159	22, 158	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ((𝑋𝐿𝑌)𝐸𝑍)) → (𝑠 ∈ (𝑋𝐿𝑌) ∨ 𝑠((hpG‘𝐺)‘(𝑋𝐿𝑌))𝑍 ∨ 𝑠𝑂𝑍))
160		3orass 1106	. . . . . 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 3943	1 ⊢ (𝜑 → ((𝑋𝐿𝑌)𝐸𝑍) ⊆ ((𝑍𝐿𝑌)𝐸𝑋))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 ∨ w3o 1102 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∃wrex 3089 ∖ cdif 3902 ⊆ wss 3905 class class class wbr 5109 {copab 5173 ran crn 5662 ‘cfv 6536 (class class class)co 7410 Basecbs 17264 distcds 17314 TarskiGcstrkg 28696 Itvcitv 28702 LineGclng 28703 hpGchpg 29039 hlGcplng 29055

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-oadd 8453 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-fz 13531 df-fzo 13679 df-hash 14363 df-word 14547 df-concat 14604 df-s1 14630 df-s2 14881 df-s3 14882 df-trkgc 28717 df-trkgb 28718 df-trkgcb 28719 df-trkgld 28721 df-trkg 28722 df-cgrg 28780 df-leg 28852 df-hlg 28870 df-mir 28930 df-rag 28974 df-perpg 28976 df-hpg 29040 df-plng 29056

This theorem is referenced by: plngrotlem3 29071

W3C validator