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 28547

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 2727	. . . 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 2727	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
17		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
18	1, 16, 2, 5, 13, 11, 7, 17	tgbtwncom 28279	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19		hlpasch.8	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))
20	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
21	1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20	outpasch 28546	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22		hlpasch.k	. . . . . . 7 ⊢ 𝐾 = (hlG‘𝐺)
23		simplr 768	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ 𝑃)
24	13	ad2antrr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵 ∈ 𝑃)
25	15	ad2antrr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ 𝑃)
26	5	ad2antrr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27		simprr 772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
28	1, 16, 2, 26, 24, 25, 23, 27	tgbtwncom 28279	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
29	26	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
30	24	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
31	25	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ 𝑃)
32		simplrr 777	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
34	33	oveq2d 7430	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
35	32, 34	eleqtrd 2830	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
36	1, 16, 2, 29, 30, 31, 35	axtgbtwnid 28257	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
37	36	eqcomd 2733	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38		hlpasch.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	38	ad3antrrr 729	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ≠ 𝐵)
40	39	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ≠ 𝐵)
41	40	neneqd 2940	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
42	37, 41	pm2.65da 816	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
43	42	neqned 2942	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ≠ 𝐵)
44	1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39	btwnhl2 28404	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾‘𝐵)𝑒)
45	7	ad2antrr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷 ∈ 𝑃)
46	9	ad2antrr 725	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋 ∈ 𝑃)
47		simprl 770	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
48	1, 16, 2, 26, 45, 23, 46, 47	tgbtwncom 28279	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
49	44, 48	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
50	49	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
51	50	reximdva 3163	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
52	21, 51	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
53	6	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃)
54	53	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ 𝑃)
55		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
56	55	breq2d 5154	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
57	55	eleq1d 2813	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
58	56, 57	anbi12d 630	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
59	14	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃)
60	59	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ 𝑃)
61	12	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵 ∈ 𝑃)
62	61	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵 ∈ 𝑃)
63	4	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
64	63	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65		hlpasch.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
66	1, 2, 22, 10, 6, 12, 4, 65	hlcomd 28395	. . . . . . . . 9 ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐶)
67	66	ad3antrrr 729	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
68	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶 ∈ 𝑃)
69	68	ad2antrr 725	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ∈ 𝑃)
70	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
71	70	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
73	72	oveq1d 7429	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
74	71, 73	eleqtrd 2830	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
75	1, 2, 22, 10, 6, 12, 4	ishlg 28393	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐷 ↔ (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
76	65, 75	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
77	76	simp1d 1140	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
78	77	ad3antrrr 729	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ≠ 𝐵)
79	38	ad2antrr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ≠ 𝐵)
80	79	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ≠ 𝐵)
81	1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80	hlbtwn 28402	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾‘𝐵)𝐶 ↔ 𝐷(𝐾‘𝐵)𝐴))
82	67, 81	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐴)
83	1, 2, 22, 54, 60, 62, 64, 82	hlcomd 28395	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾‘𝐵)𝐷)
84	8	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ 𝑃)
85	84	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 ∈ 𝑃)
86	1, 16, 2, 64, 85, 54	tgbtwntriv2 28278	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
87	83, 86	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
88	54, 58, 87	rspcedvd 3609	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
89	84	ad2antrr 725	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ 𝑃)
90		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
91	90	breq2d 5154	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝑋))
92	90	eleq1d 2813	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
93	91, 92	anbi12d 630	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
94	93	ad4ant14 751	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
95		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝐴(𝐾‘𝐵)𝑋)
96	1, 16, 2, 63, 84, 53	tgbtwntriv1 28282	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
97	96	ad2antrr 725	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
98	95, 97	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷)))
99	89, 94, 98	rspcedvd 3609	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
100	53	ad2antrr 725	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ 𝑃)
101		simpr 484	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102	101	breq2d 5154	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
103	101	eleq1d 2813	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104	102, 103	anbi12d 630	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
105	79	ad2antrr 725	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ≠ 𝐵)
106	1, 2, 22, 10, 6, 12, 4, 65	hlne2 28397	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐵)
107	106	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ≠ 𝐵)
108	63	ad2antrr 725	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
109	61	ad2antrr 725	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ 𝑃)
110	59	ad2antrr 725	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ 𝑃)
111	68	ad2antrr 725	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐶 ∈ 𝑃)
112	111	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶 ∈ 𝑃)
113	84	ad2antrr 725	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋 ∈ 𝑃)
114		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
115	70	ad2antrr 725	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116	115	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
117	1, 16, 2, 108, 113, 109, 110, 112, 114, 116	tgbtwnexch3 28285	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118		simp-4r 783	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
119	1, 2, 108, 109, 110, 100, 112, 117, 118	tgbtwnconn3 28368	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120	1, 2, 22, 14, 6, 12, 4	ishlg 28393	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121	120	ad4antr 731	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122	105, 107, 119, 121	mpbir3and 1340	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾‘𝐵)𝐷)
123	1, 16, 2, 108, 113, 100	tgbtwntriv2 28278	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124	122, 123	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
125	100, 104, 124	rspcedvd 3609	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
126	8	ad3antrrr 729	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ 𝑃)
127	12	ad3antrrr 729	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ∈ 𝑃)
128	14	ad3antrrr 729	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ 𝑃)
129	4	ad3antrrr 729	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
130		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ≠ 𝐵)
131	130	neneqd 2940	. . . . . . 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 7430	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139	136, 138	eleqtrrd 2831	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
140	1, 16, 2, 133, 134, 135, 139	axtgbtwnid 28257	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141	140	olcd 873	. . . . . . . . . . . 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 2991	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ≠ 𝑋)
149	148	neneqd 2940	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → ¬ 𝐶 = 𝑋)
150	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ 𝑃)
151	106	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ≠ 𝐵)
152		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
153	1, 2, 3, 132, 150, 127, 126, 151, 152	lncom 28413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
154	77	necomd 2991	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
155	154	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ≠ 𝐶)
156	66	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
157	1, 2, 22, 150, 111, 127, 132, 3, 156	hlln 28398	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
158	1, 2, 3, 132, 127, 111, 150, 155, 157	lncom 28413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159	158	orcd 872	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
160	1, 2, 3, 132, 126, 150, 127, 111, 153, 159	coltr 28438	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
161	1, 3, 2, 132, 127, 111, 126, 160	colrot1 28350	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162	161	orcomd 870	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164	163	ord 863	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (¬ 𝐶 = 𝑋 → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165	149, 164	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
166	1, 3, 2, 132, 126, 128, 111, 115	btwncolg3 28348	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167	166	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168	1, 2, 3, 142, 143, 144, 145, 146, 165, 167	coltr 28438	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169	141, 168	pm2.61dane 3024	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170	1, 3, 2, 132, 126, 128, 127, 169	colrot2 28351	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
171	1, 3, 2, 132, 127, 126, 128, 170	colcom 28349	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172	171	orcomd 870	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 = 𝐵 ∨ 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173	172	ord 863	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (¬ 𝑋 = 𝐵 → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174	131, 173	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
175	1, 2, 22, 126, 127, 128, 129, 128, 3, 174	lnhl 28406	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴(𝐾‘𝐵)𝑋 ∨ 𝐵 ∈ (𝑋𝐼𝐴)))
176	99, 125, 175	mpjaodan 957	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
177	88, 176	pm2.61dane 3024	. . 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 28258	. . . . 5 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185	184	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186		simplr 768	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ 𝑃)
187	181	ad3antrrr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴 ∈ 𝑃)
188	180	ad3antrrr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ∈ 𝑃)
189	178	ad3antrrr 729	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190		simprl 770	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
191	1, 16, 2, 189, 187, 186, 188, 190	tgbtwncom 28279	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
192	38	necomd 2991	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
193	192	ad4antr 731	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ≠ 𝐴)
194	189	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
195	6	ad5antr 733	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ 𝑃)
196	8	ad5antr 733	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋 ∈ 𝑃)
197	188	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
198		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199	106	necomd 2991	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐷)
200	199	ad5antr 733	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
201	200	neneqd 2940	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202		ioran 982	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203	198, 201, 202	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
204	1, 3, 2, 194, 197, 195, 196, 203	ncolrot2 28354	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206	186	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ 𝑃)
207	1, 2, 3, 194, 195, 196, 197, 204	ncolne1 28416	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝑋)
208		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
209	1, 2, 3, 194, 195, 196, 206, 207, 208	btwnlng1 28410	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210	205, 209	eqeltrrd 2829	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
211	1, 2, 3, 194, 195, 196, 207	tglinerflx1 28424	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212	106	ad5antr 733	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝐵)
213	212	necomd 2991	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
214	1, 2, 3, 194, 197, 195, 213	tglinerflx1 28424	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
215	1, 2, 3, 194, 197, 195, 213	tglinerflx2 28425	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
216	1, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215	tglineinteq 28436	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217	216, 201	pm2.65da 816	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218	217	neqned 2942	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ≠ 𝐵)
219	1, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218	btwnhl1 28403	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾‘𝐵)𝐴)
220	1, 2, 22, 186, 187, 188, 189, 219	hlcomd 28395	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾‘𝐵)𝑒)
221	178	ad3antrrr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222	182	ad3antrrr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷 ∈ 𝑃)
223		simplr 768	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ 𝑃)
224	179	ad3antrrr 729	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋 ∈ 𝑃)
225		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
226	1, 16, 2, 221, 222, 223, 224, 225	tgbtwncom 28279	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227	226	adantrl 715	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228	220, 227	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
229	228	ex 412	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
230	229	reximdva 3163	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
231	185, 230	mpd 15	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
232	177, 231	pm2.61dan 812	. 2 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
233	76	simp3d 1142	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
234	52, 232, 233	mpjaodan 957	1 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ≠ wne 2935 ∃wrex 3065 class class class wbr 5142 ‘cfv 6542 (class class class)co 7414 Basecbs 17171 distcds 17233 TarskiGcstrkg 28218 Itvcitv 28224 LineGclng 28225 hlGchlg 28391

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2164 ax-ext 2698 ax-rep 5279 ax-sep 5293 ax-nul 5300 ax-pow 5359 ax-pr 5423 ax-un 7734 ax-cnex 11186 ax-resscn 11187 ax-1cn 11188 ax-icn 11189 ax-addcl 11190 ax-addrcl 11191 ax-mulcl 11192 ax-mulrcl 11193 ax-mulcom 11194 ax-addass 11195 ax-mulass 11196 ax-distr 11197 ax-i2m1 11198 ax-1ne0 11199 ax-1rid 11200 ax-rnegex 11201 ax-rrecex 11202 ax-cnre 11203 ax-pre-lttri 11204 ax-pre-lttrn 11205 ax-pre-ltadd 11206 ax-pre-mulgt0 11207

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ne 2936 df-nel 3042 df-ral 3057 df-rex 3066 df-rmo 3371 df-reu 3372 df-rab 3428 df-v 3471 df-sbc 3775 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5143 df-opab 5205 df-mpt 5226 df-tr 5260 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7865 df-1st 7987 df-2nd 7988 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8718 df-map 8838 df-pm 8839 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-dju 9916 df-card 9954 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11468 df-neg 11469 df-nn 12235 df-2 12297 df-3 12298 df-n0 12495 df-xnn0 12567 df-z 12581 df-uz 12845 df-fz 13509 df-fzo 13652 df-hash 14314 df-word 14489 df-concat 14545 df-s1 14570 df-s2 14823 df-s3 14824 df-trkgc 28239 df-trkgb 28240 df-trkgcb 28241 df-trkgld 28243 df-trkg 28244 df-cgrg 28302 df-leg 28374 df-hlg 28392 df-mir 28444 df-rag 28485 df-perpg 28487

This theorem is referenced by: inaghl 28636

W3C validator