hlpasch - Metamath Proof Explorer

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

Theorem hlpasch 28812

Description: An application of the axiom of Pasch for half-lines. (Contributed by Thierry Arnoux, 15-Sep-2020.)

**Hypotheses**
Ref	Expression
hlpasch.p	⊢ 𝑃 = (Base‘𝐺)
hlpasch.i	⊢ 𝐼 = (Itv‘𝐺)
hlpasch.k	⊢ 𝐾 = (hlG‘𝐺)
hlpasch.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
hlpasch.1	⊢ (𝜑 → 𝐴 ∈ 𝑃)
hlpasch.2	⊢ (𝜑 → 𝐵 ∈ 𝑃)
hlpasch.3	⊢ (𝜑 → 𝐶 ∈ 𝑃)
hlpasch.4	⊢ (𝜑 → 𝑋 ∈ 𝑃)
hlpasch.5	⊢ (𝜑 → 𝐷 ∈ 𝑃)
hlpasch.6	⊢ (𝜑 → 𝐴 ≠ 𝐵)
hlpasch.7	⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
hlpasch.8	⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))

**Assertion**
Ref	Expression
hlpasch	⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Distinct variable groups: 𝐴,𝑒 𝐵,𝑒 𝐶,𝑒 𝐷,𝑒 𝑒,𝐺 𝑒,𝐼 𝑒,𝐾 𝑃,𝑒 𝑒,𝑋 𝜑,𝑒

**Proof of Theorem hlpasch**
Step	Hyp	Ref	Expression
1		hlpasch.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
2		hlpasch.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
3		eqid 2737	. . . 4 ⊢ (LineG‘𝐺) = (LineG‘𝐺)
4		hlpasch.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐺 ∈ TarskiG)
6		hlpasch.5	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐷 ∈ 𝑃)
8		hlpasch.4	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9	8	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝑋 ∈ 𝑃)
10		hlpasch.3	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ 𝑃)
12		hlpasch.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
13	12	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐵 ∈ 𝑃)
14		hlpasch.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
15	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ 𝑃)
16		eqid 2737	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
17		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
18	1, 16, 2, 5, 13, 11, 7, 17	tgbtwncom 28544	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19		hlpasch.8	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))
20	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
21	1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20	outpasch 28811	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22		hlpasch.k	. . . . . . 7 ⊢ 𝐾 = (hlG‘𝐺)
23		simplr 769	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ 𝑃)
24	13	ad2antrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵 ∈ 𝑃)
25	15	ad2antrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ 𝑃)
26	5	ad2antrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27		simprr 773	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
28	1, 16, 2, 26, 24, 25, 23, 27	tgbtwncom 28544	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
29	26	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
30	24	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
31	25	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ 𝑃)
32		simplrr 778	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
34	33	oveq2d 7374	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
35	32, 34	eleqtrd 2839	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
36	1, 16, 2, 29, 30, 31, 35	axtgbtwnid 28522	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
37	36	eqcomd 2743	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38		hlpasch.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	38	ad3antrrr 731	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ≠ 𝐵)
40	39	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ≠ 𝐵)
41	40	neneqd 2938	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
42	37, 41	pm2.65da 817	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
43	42	neqned 2940	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ≠ 𝐵)
44	1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39	btwnhl2 28669	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾‘𝐵)𝑒)
45	7	ad2antrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷 ∈ 𝑃)
46	9	ad2antrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋 ∈ 𝑃)
47		simprl 771	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
48	1, 16, 2, 26, 45, 23, 46, 47	tgbtwncom 28544	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
49	44, 48	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
50	49	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
51	50	reximdva 3151	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
52	21, 51	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
53	6	ad2antrr 727	. . . . . 6 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃)
54	53	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ 𝑃)
55		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
56	55	breq2d 5098	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
57	55	eleq1d 2822	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
58	56, 57	anbi12d 633	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
59	14	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃)
60	59	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ 𝑃)
61	12	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵 ∈ 𝑃)
62	61	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵 ∈ 𝑃)
63	4	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
64	63	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65		hlpasch.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
66	1, 2, 22, 10, 6, 12, 4, 65	hlcomd 28660	. . . . . . . . 9 ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐶)
67	66	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
68	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶 ∈ 𝑃)
69	68	ad2antrr 727	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ∈ 𝑃)
70	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
71	70	ad2antrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
73	72	oveq1d 7373	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
74	71, 73	eleqtrd 2839	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
75	1, 2, 22, 10, 6, 12, 4	ishlg 28658	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐷 ↔ (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
76	65, 75	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
77	76	simp1d 1143	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
78	77	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ≠ 𝐵)
79	38	ad2antrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ≠ 𝐵)
80	79	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ≠ 𝐵)
81	1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80	hlbtwn 28667	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾‘𝐵)𝐶 ↔ 𝐷(𝐾‘𝐵)𝐴))
82	67, 81	mpbid 232	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐴)
83	1, 2, 22, 54, 60, 62, 64, 82	hlcomd 28660	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾‘𝐵)𝐷)
84	8	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ 𝑃)
85	84	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 ∈ 𝑃)
86	1, 16, 2, 64, 85, 54	tgbtwntriv2 28543	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
87	83, 86	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
88	54, 58, 87	rspcedvd 3567	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
89	84	ad2antrr 727	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ 𝑃)
90		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
91	90	breq2d 5098	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝑋))
92	90	eleq1d 2822	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
93	91, 92	anbi12d 633	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
94	93	ad4ant14 753	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
95		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝐴(𝐾‘𝐵)𝑋)
96	1, 16, 2, 63, 84, 53	tgbtwntriv1 28547	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
97	96	ad2antrr 727	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
98	95, 97	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷)))
99	89, 94, 98	rspcedvd 3567	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
100	53	ad2antrr 727	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ 𝑃)
101		simpr 484	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102	101	breq2d 5098	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
103	101	eleq1d 2822	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104	102, 103	anbi12d 633	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
105	79	ad2antrr 727	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ≠ 𝐵)
106	1, 2, 22, 10, 6, 12, 4, 65	hlne2 28662	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐵)
107	106	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ≠ 𝐵)
108	63	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
109	61	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ 𝑃)
110	59	ad2antrr 727	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ 𝑃)
111	68	ad2antrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐶 ∈ 𝑃)
112	111	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶 ∈ 𝑃)
113	84	ad2antrr 727	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋 ∈ 𝑃)
114		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
115	70	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116	115	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
117	1, 16, 2, 108, 113, 109, 110, 112, 114, 116	tgbtwnexch3 28550	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118		simp-4r 784	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
119	1, 2, 108, 109, 110, 100, 112, 117, 118	tgbtwnconn3 28633	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120	1, 2, 22, 14, 6, 12, 4	ishlg 28658	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121	120	ad4antr 733	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122	105, 107, 119, 121	mpbir3and 1344	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾‘𝐵)𝐷)
123	1, 16, 2, 108, 113, 100	tgbtwntriv2 28543	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124	122, 123	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
125	100, 104, 124	rspcedvd 3567	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
126	8	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ 𝑃)
127	12	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ∈ 𝑃)
128	14	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ 𝑃)
129	4	ad3antrrr 731	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
130		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ≠ 𝐵)
131	130	neneqd 2938	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ¬ 𝑋 = 𝐵)
132	63	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
133	132	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
134	126	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 ∈ 𝑃)
135	128	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ 𝑃)
136	115	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
137		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
138	137	oveq2d 7374	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139	136, 138	eleqtrrd 2840	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
140	1, 16, 2, 133, 134, 135, 139	axtgbtwnid 28522	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141	140	olcd 875	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
142	132	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐺 ∈ TarskiG)
143	127	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ 𝑃)
144	111	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ∈ 𝑃)
145	126	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝑋 ∈ 𝑃)
146	128	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐴 ∈ 𝑃)
147		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝑋 ≠ 𝐶)
148	147	necomd 2988	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ≠ 𝑋)
149	148	neneqd 2938	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → ¬ 𝐶 = 𝑋)
150	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ 𝑃)
151	106	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ≠ 𝐵)
152		simplr 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
153	1, 2, 3, 132, 150, 127, 126, 151, 152	lncom 28678	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
154	77	necomd 2988	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
155	154	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ≠ 𝐶)
156	66	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
157	1, 2, 22, 150, 111, 127, 132, 3, 156	hlln 28663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
158	1, 2, 3, 132, 127, 111, 150, 155, 157	lncom 28678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159	158	orcd 874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
160	1, 2, 3, 132, 126, 150, 127, 111, 153, 159	coltr 28703	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
161	1, 3, 2, 132, 127, 111, 126, 160	colrot1 28615	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162	161	orcomd 872	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164	163	ord 865	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (¬ 𝐶 = 𝑋 → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165	149, 164	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
166	1, 3, 2, 132, 126, 128, 111, 115	btwncolg3 28613	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167	166	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168	1, 2, 3, 142, 143, 144, 145, 146, 165, 167	coltr 28703	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169	141, 168	pm2.61dane 3020	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170	1, 3, 2, 132, 126, 128, 127, 169	colrot2 28616	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
171	1, 3, 2, 132, 127, 126, 128, 170	colcom 28614	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172	171	orcomd 872	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 = 𝐵 ∨ 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173	172	ord 865	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (¬ 𝑋 = 𝐵 → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174	131, 173	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
175	1, 2, 22, 126, 127, 128, 129, 128, 3, 174	lnhl 28671	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴(𝐾‘𝐵)𝑋 ∨ 𝐵 ∈ (𝑋𝐼𝐴)))
176	99, 125, 175	mpjaodan 961	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
177	88, 176	pm2.61dane 3020	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
178	4	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
179	8	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋 ∈ 𝑃)
180	12	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵 ∈ 𝑃)
181	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ 𝑃)
182	6	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ 𝑃)
183		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
184	1, 16, 2, 178, 179, 180, 68, 181, 182, 70, 183	axtgpasch 28523	. . . . 5 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185	184	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186		simplr 769	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ 𝑃)
187	181	ad3antrrr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴 ∈ 𝑃)
188	180	ad3antrrr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ∈ 𝑃)
189	178	ad3antrrr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190		simprl 771	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
191	1, 16, 2, 189, 187, 186, 188, 190	tgbtwncom 28544	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
192	38	necomd 2988	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
193	192	ad4antr 733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ≠ 𝐴)
194	189	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
195	6	ad5antr 735	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ 𝑃)
196	8	ad5antr 735	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋 ∈ 𝑃)
197	188	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
198		simp-4r 784	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199	106	necomd 2988	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐷)
200	199	ad5antr 735	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
201	200	neneqd 2938	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202		ioran 986	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203	198, 201, 202	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
204	1, 3, 2, 194, 197, 195, 196, 203	ncolrot2 28619	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206	186	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ 𝑃)
207	1, 2, 3, 194, 195, 196, 197, 204	ncolne1 28681	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝑋)
208		simplrr 778	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
209	1, 2, 3, 194, 195, 196, 206, 207, 208	btwnlng1 28675	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210	205, 209	eqeltrrd 2838	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
211	1, 2, 3, 194, 195, 196, 207	tglinerflx1 28689	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212	106	ad5antr 735	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝐵)
213	212	necomd 2988	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
214	1, 2, 3, 194, 197, 195, 213	tglinerflx1 28689	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
215	1, 2, 3, 194, 197, 195, 213	tglinerflx2 28690	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
216	1, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215	tglineinteq 28701	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217	216, 201	pm2.65da 817	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218	217	neqned 2940	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ≠ 𝐵)
219	1, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218	btwnhl1 28668	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾‘𝐵)𝐴)
220	1, 2, 22, 186, 187, 188, 189, 219	hlcomd 28660	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾‘𝐵)𝑒)
221	178	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222	182	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷 ∈ 𝑃)
223		simplr 769	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ 𝑃)
224	179	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋 ∈ 𝑃)
225		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
226	1, 16, 2, 221, 222, 223, 224, 225	tgbtwncom 28544	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227	226	adantrl 717	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228	220, 227	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
229	228	ex 412	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
230	229	reximdva 3151	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
231	185, 230	mpd 15	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
232	177, 231	pm2.61dan 813	. 2 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
233	76	simp3d 1145	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
234	52, 232, 233	mpjaodan 961	1 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 class class class wbr 5086 ‘cfv 6490 (class class class)co 7358 Basecbs 17137 distcds 17187 TarskiGcstrkg 28483 Itvcitv 28489 LineGclng 28490 hlGchlg 28656

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-tp 4573 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-oadd 8400 df-er 8634 df-map 8766 df-pm 8767 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-dju 9814 df-card 9852 df-pnf 11169 df-mnf 11170 df-xr 11171 df-ltxr 11172 df-le 11173 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-3 12210 df-n0 12403 df-xnn0 12476 df-z 12490 df-uz 12753 df-fz 13425 df-fzo 13572 df-hash 14255 df-word 14438 df-concat 14495 df-s1 14521 df-s2 14772 df-s3 14773 df-trkgc 28504 df-trkgb 28505 df-trkgcb 28506 df-trkgld 28508 df-trkg 28509 df-cgrg 28567 df-leg 28639 df-hlg 28657 df-mir 28709 df-rag 28750 df-perpg 28752

This theorem is referenced by: inaghl 28901

W3C validator