Theorem lnopp2hpgb 28835

Description: Theorem 9.8 of [Schwabhauser] p. 71. (Contributed by Thierry Arnoux, 4-Mar-2020.)

Hypotheses

Ref	Expression
ishpg.p	⊢ 𝑃 = (Base‘𝐺)
ishpg.i	⊢ 𝐼 = (Itv‘𝐺)
ishpg.l	⊢ 𝐿 = (LineG‘𝐺)
ishpg.o	⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
ishpg.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
ishpg.d	⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
hpgbr.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
hpgbr.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
lnopp2hpgb.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
lnopp2hpgb.1	⊢ (𝜑 → 𝐴𝑂𝐶)

Assertion

Ref	Expression
lnopp2hpgb	⊢ (𝜑 → (𝐵𝑂𝐶 ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵))

Distinct variable groups:   𝑡,𝐴   𝑡,𝐵   𝐶,𝑎,𝑏,𝑡   𝐷,𝑎,𝑏,𝑡   𝐺,𝑎,𝑏,𝑡   𝐼,𝑎,𝑏,𝑡   𝐿,𝑎,𝑏,𝑡   𝑂,𝑎,𝑏,𝑡   𝑃,𝑎,𝑏,𝑡   𝜑,𝑡

Allowed substitution hints:   𝜑(𝑎,𝑏)   𝐴(𝑎,𝑏)   𝐵(𝑎,𝑏)

Proof of Theorem lnopp2hpgb

Dummy variables 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lnopp2hpgb.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
2	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → 𝐶 ∈ 𝑃)
3		lnopp2hpgb.1	. . . . 5 ⊢ (𝜑 → 𝐴𝑂𝐶)
4	3	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → 𝐴𝑂𝐶)
5		simpr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → 𝐵𝑂𝐶)
6		breq2 5102	. . . . . 6 ⊢ (𝑑 = 𝐶 → (𝐴𝑂𝑑 ↔ 𝐴𝑂𝐶))
7		breq2 5102	. . . . . 6 ⊢ (𝑑 = 𝐶 → (𝐵𝑂𝑑 ↔ 𝐵𝑂𝐶))
8	6, 7	anbi12d 632	. . . . 5 ⊢ (𝑑 = 𝐶 → ((𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑) ↔ (𝐴𝑂𝐶 ∧ 𝐵𝑂𝐶)))
9	8	rspcev 3576	. . . 4 ⊢ ((𝐶 ∈ 𝑃 ∧ (𝐴𝑂𝐶 ∧ 𝐵𝑂𝐶)) → ∃𝑑 ∈ 𝑃 (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑))
10	2, 4, 5, 9	syl12anc 836	. . 3 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → ∃𝑑 ∈ 𝑃 (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑))
11		ishpg.p	. . . . 5 ⊢ 𝑃 = (Base‘𝐺)
12		ishpg.i	. . . . 5 ⊢ 𝐼 = (Itv‘𝐺)
13		ishpg.l	. . . . 5 ⊢ 𝐿 = (LineG‘𝐺)
14		ishpg.o	. . . . 5 ⊢ 𝑂 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))}
15		ishpg.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
16		ishpg.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ ran 𝐿)
17		hpgbr.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
18		hpgbr.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
19	11, 12, 13, 14, 15, 16, 17, 18	hpgbr 28832	. . . 4 ⊢ (𝜑 → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ ∃𝑑 ∈ 𝑃 (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)))
20	19	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → (𝐴((hpG‘𝐺)‘𝐷)𝐵 ↔ ∃𝑑 ∈ 𝑃 (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)))
21	10, 20	mpbird 257	. 2 ⊢ ((𝜑 ∧ 𝐵𝑂𝐶) → 𝐴((hpG‘𝐺)‘𝐷)𝐵)
22		eqid 2736	. . . . . . . 8 ⊢ (dist‘𝐺) = (dist‘𝐺)
23	16	ad7antr 738	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐷 ∈ ran 𝐿)
24	23	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐷 ∈ ran 𝐿)
25	15	ad7antr 738	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐺 ∈ TarskiG)
26	25	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐺 ∈ TarskiG)
27		eqid 2736	. . . . . . . 8 ⊢ (hlG‘𝐺) = (hlG‘𝐺)
28	17	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝐴 ∈ 𝑃)
29	28	ad4antr 732	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐴 ∈ 𝑃)
30	29	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴 ∈ 𝑃)
31	18	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝐵 ∈ 𝑃)
32	31	ad4antr 732	. . . . . . . . 9 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐵 ∈ 𝑃)
33	32	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐵 ∈ 𝑃)
34	1	ad10antr 744	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐶 ∈ 𝑃)
35	3	ad10antr 744	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴𝑂𝐶)
36		simpr 484	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝐷)
37		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦 ∈ 𝐷)
38	11, 13, 12, 25, 23, 37	tglnpt 28621	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦 ∈ 𝑃)
39	38	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ 𝑃)
40		simp-5r 785	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ 𝐷)
41	11, 22, 12, 14, 13, 24, 26, 30, 34, 35	oppne1 28813	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → ¬ 𝐴 ∈ 𝐷)
42		nelne2 3030	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷) → 𝑦 ≠ 𝐴)
43	40, 41, 42	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ≠ 𝐴)
44	11, 12, 13, 26, 39, 30, 43	tgelrnln 28702	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝑦𝐿𝐴) ∈ ran 𝐿)
45	11, 12, 13, 26, 39, 30, 43	tglinerflx2 28706	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴 ∈ (𝑦𝐿𝐴))
46		nelne1 3029	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ (𝑦𝐿𝐴) ∧ ¬ 𝐴 ∈ 𝐷) → (𝑦𝐿𝐴) ≠ 𝐷)
47	45, 41, 46	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝑦𝐿𝐴) ≠ 𝐷)
48	47	necomd 2987	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐷 ≠ (𝑦𝐿𝐴))
49		simpllr 775	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝑃)
50		simplrr 777	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑦𝐼𝐴))
51	11, 12, 13, 26, 39, 30, 49, 43, 50	btwnlng1 28691	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑦𝐿𝐴))
52	36, 51	elind 4152	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝐷 ∩ (𝑦𝐿𝐴)))
53	11, 12, 13, 26, 39, 30, 43	tglinerflx1 28705	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ (𝑦𝐿𝐴))
54	40, 53	elind 4152	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ (𝐷 ∩ (𝑦𝐿𝐴)))
55	11, 12, 13, 26, 24, 44, 48, 52, 54	tglineineq 28715	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 = 𝑦)
56	55, 43	eqnetrd 2999	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ≠ 𝐴)
57	56	necomd 2987	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴 ≠ 𝑧)
58		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥 ∈ 𝐷)
59	11, 13, 12, 25, 23, 58	tglnpt 28621	. . . . . . . . . . . . . 14 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥 ∈ 𝑃)
60	59	ad3antrrr 730	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ 𝑃)
61		simp-7r 789	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ 𝐷)
62		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝑑 ∈ 𝑃)
63	62	ad4antr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑑 ∈ 𝑃)
64	63	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑑 ∈ 𝑃)
65		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝐵𝑂𝑑)
66	65	ad7antr 738	. . . . . . . . . . . . . . 15 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐵𝑂𝑑)
67	11, 22, 12, 14, 13, 24, 26, 33, 64, 66	oppne1 28813	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → ¬ 𝐵 ∈ 𝐷)
68		nelne2 3030	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) → 𝑥 ≠ 𝐵)
69	61, 67, 68	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ≠ 𝐵)
70	11, 12, 13, 26, 60, 33, 69	tgelrnln 28702	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝑥𝐿𝐵) ∈ ran 𝐿)
71	11, 12, 13, 26, 60, 33, 69	tglinerflx2 28706	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐵 ∈ (𝑥𝐿𝐵))
72		nelne1 3029	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ (𝑥𝐿𝐵) ∧ ¬ 𝐵 ∈ 𝐷) → (𝑥𝐿𝐵) ≠ 𝐷)
73	71, 67, 72	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝑥𝐿𝐵) ≠ 𝐷)
74	73	necomd 2987	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐷 ≠ (𝑥𝐿𝐵))
75		simplrl 776	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑥𝐼𝐵))
76	11, 12, 13, 26, 60, 33, 49, 69, 75	btwnlng1 28691	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑥𝐿𝐵))
77	36, 76	elind 4152	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝐷 ∩ (𝑥𝐿𝐵)))
78	11, 12, 13, 26, 60, 33, 69	tglinerflx1 28705	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ (𝑥𝐿𝐵))
79	61, 78	elind 4152	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ (𝐷 ∩ (𝑥𝐿𝐵)))
80	11, 12, 13, 26, 24, 70, 74, 77, 79	tglineineq 28715	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 = 𝑥)
81	80, 69	eqnetrd 2999	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ≠ 𝐵)
82	81	necomd 2987	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐵 ≠ 𝑧)
83		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝐴𝑂𝑑)
84	83	ad7antr 738	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴𝑂𝑑)
85	11, 22, 12, 14, 13, 24, 26, 30, 64, 84	oppne2 28814	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → ¬ 𝑑 ∈ 𝐷)
86		nelne2 3030	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷) → 𝑧 ≠ 𝑑)
87	36, 85, 86	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ≠ 𝑑)
88	87	necomd 2987	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑑 ≠ 𝑧)
89		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑥 ∈ (𝐴𝐼𝑑))
90	89	ad3antrrr 730	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ (𝐴𝐼𝑑))
91	11, 22, 12, 26, 30, 60, 64, 90	tgbtwncom 28560	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑥 ∈ (𝑑𝐼𝐴))
92	80, 91	eqeltrd 2836	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑑𝐼𝐴))
93		simp-4r 783	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ (𝐵𝐼𝑑))
94	11, 22, 12, 26, 33, 39, 64, 93	tgbtwncom 28560	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑦 ∈ (𝑑𝐼𝐵))
95	55, 94	eqeltrd 2836	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑑𝐼𝐵))
96	11, 12, 26, 64, 49, 30, 33, 88, 92, 95	tgbtwnconn2 28648	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝐴 ∈ (𝑧𝐼𝐵) ∨ 𝐵 ∈ (𝑧𝐼𝐴)))
97	11, 12, 27, 30, 33, 49, 26	ishlg 28674	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → (𝐴((hlG‘𝐺)‘𝑧)𝐵 ↔ (𝐴 ≠ 𝑧 ∧ 𝐵 ≠ 𝑧 ∧ (𝐴 ∈ (𝑧𝐼𝐵) ∨ 𝐵 ∈ (𝑧𝐼𝐴)))))
98	57, 82, 96, 97	mpbir3and 1343	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐴((hlG‘𝐺)‘𝑧)𝐵)
99	11, 22, 12, 14, 13, 24, 26, 27, 30, 33, 34, 35, 36, 98	opphl 28826	. . . . . . 7 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ 𝑧 ∈ 𝐷) → 𝐵𝑂𝐶)
100	23	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐷 ∈ ran 𝐿)
101	25	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐺 ∈ TarskiG)
102		simpllr 775	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧 ∈ 𝑃)
103	32	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐵 ∈ 𝑃)
104	1	ad10antr 744	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐶 ∈ 𝑃)
105	29	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐴 ∈ 𝑃)
106	3	ad10antr 744	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐴𝑂𝐶)
107		simp-5r 785	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑦 ∈ 𝐷)
108	38	ad3antrrr 730	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑦 ∈ 𝑃)
109		simplrr 777	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑦𝐼𝐴))
110		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → ¬ 𝑧 ∈ 𝐷)
111		nelne2 3030	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐷 ∧ ¬ 𝑧 ∈ 𝐷) → 𝑦 ≠ 𝑧)
112	107, 110, 111	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑦 ≠ 𝑧)
113	112	necomd 2987	. . . . . . . . . . . 12 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧 ≠ 𝑦)
114	11, 22, 12, 101, 108, 102, 105, 109, 113	tgbtwnne 28562	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑦 ≠ 𝐴)
115	11, 12, 27, 108, 105, 102, 101, 105, 109, 114, 113	btwnhl1 28684	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧((hlG‘𝐺)‘𝑦)𝐴)
116	11, 12, 27, 102, 105, 108, 101, 115	hlcomd 28676	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐴((hlG‘𝐺)‘𝑦)𝑧)
117	11, 22, 12, 14, 13, 100, 101, 27, 105, 102, 104, 106, 107, 116	opphl 28826	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧𝑂𝐶)
118	58	ad3antrrr 730	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑥 ∈ 𝐷)
119	59	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑥 ∈ 𝑃)
120		simplrl 776	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧 ∈ (𝑥𝐼𝐵))
121		nelne2 3030	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐷 ∧ ¬ 𝑧 ∈ 𝐷) → 𝑥 ≠ 𝑧)
122	118, 110, 121	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑥 ≠ 𝑧)
123	122	necomd 2987	. . . . . . . . . 10 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧 ≠ 𝑥)
124	11, 22, 12, 101, 119, 102, 103, 120, 123	tgbtwnne 28562	. . . . . . . . 9 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑥 ≠ 𝐵)
125	11, 12, 27, 119, 103, 102, 101, 105, 120, 124, 123	btwnhl1 28684	. . . . . . . 8 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝑧((hlG‘𝐺)‘𝑥)𝐵)
126	11, 22, 12, 14, 13, 100, 101, 27, 102, 103, 104, 117, 118, 125	opphl 28826	. . . . . . 7 ⊢ (((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) ∧ ¬ 𝑧 ∈ 𝐷) → 𝐵𝑂𝐶)
127	99, 126	pm2.61dan 812	. . . . . 6 ⊢ ((((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) ∧ 𝑧 ∈ 𝑃) ∧ (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴))) → 𝐵𝑂𝐶)
128		simpr 484	. . . . . . 7 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝑦 ∈ (𝐵𝐼𝑑))
129	11, 22, 12, 25, 29, 32, 63, 59, 38, 89, 128	axtgpasch 28539	. . . . . 6 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → ∃𝑧 ∈ 𝑃 (𝑧 ∈ (𝑥𝐼𝐵) ∧ 𝑧 ∈ (𝑦𝐼𝐴)))
130	127, 129	r19.29a 3144	. . . . 5 ⊢ ((((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) ∧ 𝑦 ∈ 𝐷) ∧ 𝑦 ∈ (𝐵𝐼𝑑)) → 𝐵𝑂𝐶)
131	11, 22, 12, 14, 31, 62	islnopp 28811	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → (𝐵𝑂𝑑 ↔ ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝑑))))
132	65, 131	mpbid 232	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝑑)))
133	132	simprd 495	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝑑))
134		eleq1w 2819	. . . . . . . 8 ⊢ (𝑡 = 𝑦 → (𝑡 ∈ (𝐵𝐼𝑑) ↔ 𝑦 ∈ (𝐵𝐼𝑑)))
135	134	cbvrexvw 3215	. . . . . . 7 ⊢ (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝑑) ↔ ∃𝑦 ∈ 𝐷 𝑦 ∈ (𝐵𝐼𝑑))
136	133, 135	sylib 218	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ∃𝑦 ∈ 𝐷 𝑦 ∈ (𝐵𝐼𝑑))
137	136	ad2antrr 726	. . . . 5 ⊢ ((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) → ∃𝑦 ∈ 𝐷 𝑦 ∈ (𝐵𝐼𝑑))
138	130, 137	r19.29a 3144	. . . 4 ⊢ ((((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) ∧ 𝑥 ∈ 𝐷) ∧ 𝑥 ∈ (𝐴𝐼𝑑)) → 𝐵𝑂𝐶)
139	11, 22, 12, 14, 28, 62	islnopp 28811	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → (𝐴𝑂𝑑 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑑))))
140	83, 139	mpbid 232	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝑑 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑑)))
141	140	simprd 495	. . . . 5 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑑))
142		eleq1w 2819	. . . . . 6 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ (𝐴𝐼𝑑) ↔ 𝑥 ∈ (𝐴𝐼𝑑)))
143	142	cbvrexvw 3215	. . . . 5 ⊢ (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝑑) ↔ ∃𝑥 ∈ 𝐷 𝑥 ∈ (𝐴𝐼𝑑))
144	141, 143	sylib 218	. . . 4 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → ∃𝑥 ∈ 𝐷 𝑥 ∈ (𝐴𝐼𝑑))
145	138, 144	r19.29a 3144	. . 3 ⊢ ((((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) ∧ 𝑑 ∈ 𝑃) ∧ (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑)) → 𝐵𝑂𝐶)
146	19	biimpa 476	. . 3 ⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → ∃𝑑 ∈ 𝑃 (𝐴𝑂𝑑 ∧ 𝐵𝑂𝑑))
147	145, 146	r19.29a 3144	. 2 ⊢ ((𝜑 ∧ 𝐴((hpG‘𝐺)‘𝐷)𝐵) → 𝐵𝑂𝐶)
148	21, 147	impbida 800	1 ⊢ (𝜑 → (𝐵𝑂𝐶 ↔ 𝐴((hpG‘𝐺)‘𝐷)𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  ∃wrex 3060   ∖ cdif 3898   class class class wbr 5098  {copab 5160  ran crn 5625  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  distcds 17186  TarskiGcstrkg 28499  Itvcitv 28505  LineGclng 28506  hlGchlg 28672  hpGchpg 28829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-tp 4585  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-oadd 8401  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9813  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-2 12208  df-3 12209  df-n0 12402  df-xnn0 12475  df-z 12489  df-uz 12752  df-fz 13424  df-fzo 13571  df-hash 14254  df-word 14437  df-concat 14494  df-s1 14520  df-s2 14771  df-s3 14772  df-trkgc 28520  df-trkgb 28521  df-trkgcb 28522  df-trkgld 28524  df-trkg 28525  df-cgrg 28583  df-leg 28655  df-hlg 28673  df-mir 28725  df-rag 28766  df-perpg 28768  df-hpg 28830

This theorem is referenced by:  lnoppnhpg  28836  hpgtr  28840  colhp  28842  lnperpex  28875  trgcopyeulem  28877