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 29111

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 2762	. . . 4 ⊢ (LineG‘𝐺) = (LineG‘𝐺)
4		hlpasch.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
5	4	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐺 ∈ TarskiG)
6		hlpasch.5	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
7	6	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐷 ∈ 𝑃)
8		hlpasch.4	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
9	8	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝑋 ∈ 𝑃)
10		hlpasch.3	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
11	10	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ 𝑃)
12		hlpasch.2	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
13	12	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐵 ∈ 𝑃)
14		hlpasch.1	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
15	14	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ 𝑃)
16		eqid 2762	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
17		simpr 490	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
18	1, 16, 2, 5, 13, 11, 7, 17	tgbtwncom 28828	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19		hlpasch.8	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))
20	19	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
21	1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20	outpasch 29110	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22		hlpasch.k	. . . . . . 7 ⊢ 𝐾 = (hlG‘𝐺)
23		simplr 781	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ 𝑃)
24	13	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵 ∈ 𝑃)
25	15	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ 𝑃)
26	5	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27		simprr 785	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
28	1, 16, 2, 26, 24, 25, 23, 27	tgbtwncom 28828	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
29	26	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
30	24	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
31	25	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ 𝑃)
32		simplrr 790	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33		simpr 490	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
34	33	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
35	32, 34	eleqtrd 2864	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
36	1, 16, 2, 29, 30, 31, 35	axtgbtwnid 28805	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
37	36	eqcomd 2768	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38		hlpasch.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	38	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ≠ 𝐵)
40	39	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ≠ 𝐵)
41	40	neneqd 2962	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
42	37, 41	pm2.65da 829	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
43	42	neqned 2964	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ≠ 𝐵)
44	1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39	btwnhl2 28956	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾‘𝐵)𝑒)
45	7	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷 ∈ 𝑃)
46	9	ad2antrr 739	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋 ∈ 𝑃)
47		simprl 783	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
48	1, 16, 2, 26, 45, 23, 46, 47	tgbtwncom 28828	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
49	44, 48	jca 521	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
50	49	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
51	50	reximdva 3177	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
52	21, 51	mpd 16	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
53	6	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃)
54	53	adantr 486	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ 𝑃)
55		simpr 490	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
56	55	breq2d 5119	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
57	55	eleq1d 2847	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
58	56, 57	anbi12d 644	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
59	14	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃)
60	59	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ 𝑃)
61	12	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵 ∈ 𝑃)
62	61	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵 ∈ 𝑃)
63	4	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
64	63	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65		hlpasch.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
66	1, 2, 22, 10, 6, 12, 4, 65	hlcomd 28947	. . . . . . . . 9 ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐶)
67	66	ad3antrrr 743	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
68	10	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶 ∈ 𝑃)
69	68	ad2antrr 739	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ∈ 𝑃)
70	19	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
71	70	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72		simpr 490	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
73	72	oveq1d 7431	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
74	71, 73	eleqtrd 2864	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
75	1, 2, 22, 10, 6, 12, 4	ishlg 28945	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐷 ↔ (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
76	65, 75	mpbid 235	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
77	76	simp1d 1160	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
78	77	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ≠ 𝐵)
79	38	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ≠ 𝐵)
80	79	adantr 486	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ≠ 𝐵)
81	1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80	hlbtwn 28954	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾‘𝐵)𝐶 ↔ 𝐷(𝐾‘𝐵)𝐴))
82	67, 81	mpbid 235	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐴)
83	1, 2, 22, 54, 60, 62, 64, 82	hlcomd 28947	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾‘𝐵)𝐷)
84	8	ad2antrr 739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ 𝑃)
85	84	adantr 486	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 ∈ 𝑃)
86	1, 16, 2, 64, 85, 54	tgbtwntriv2 28827	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
87	83, 86	jca 521	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
88	54, 58, 87	rspcedvd 3581	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
89	84	ad2antrr 739	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ 𝑃)
90		simpr 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
91	90	breq2d 5119	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝑋))
92	90	eleq1d 2847	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
93	91, 92	anbi12d 644	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
94	93	ad4ant14 765	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
95		simpr 490	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝐴(𝐾‘𝐵)𝑋)
96	1, 16, 2, 63, 84, 53	tgbtwntriv1 28831	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
97	96	ad2antrr 739	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
98	95, 97	jca 521	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷)))
99	89, 94, 98	rspcedvd 3581	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
100	53	ad2antrr 739	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ 𝑃)
101		simpr 490	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102	101	breq2d 5119	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
103	101	eleq1d 2847	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104	102, 103	anbi12d 644	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
105	79	ad2antrr 739	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ≠ 𝐵)
106	1, 2, 22, 10, 6, 12, 4, 65	hlne2 28949	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐵)
107	106	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ≠ 𝐵)
108	63	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
109	61	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ 𝑃)
110	59	ad2antrr 739	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ 𝑃)
111	68	ad2antrr 739	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐶 ∈ 𝑃)
112	111	adantr 486	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶 ∈ 𝑃)
113	84	ad2antrr 739	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋 ∈ 𝑃)
114		simpr 490	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
115	70	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116	115	adantr 486	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
117	1, 16, 2, 108, 113, 109, 110, 112, 114, 116	tgbtwnexch3 28834	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118		simp-4r 796	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
119	1, 2, 108, 109, 110, 100, 112, 117, 118	tgbtwnconn3 28917	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120	1, 2, 22, 14, 6, 12, 4	ishlg 28945	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121	120	ad4antr 745	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122	105, 107, 119, 121	mpbir3and 1361	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾‘𝐵)𝐷)
123	1, 16, 2, 108, 113, 100	tgbtwntriv2 28827	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124	122, 123	jca 521	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
125	100, 104, 124	rspcedvd 3581	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
126	8	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ 𝑃)
127	12	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ∈ 𝑃)
128	14	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ 𝑃)
129	4	ad3antrrr 743	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
130		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ≠ 𝐵)
131	130	neneqd 2962	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ¬ 𝑋 = 𝐵)
132	63	adantr 486	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
133	132	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐺 ∈ TarskiG)
134	126	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 ∈ 𝑃)
135	128	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ 𝑃)
136	115	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝐶))
137		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐶)
138	137	oveq2d 7432	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139	136, 138	eleqtrrd 2865	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
140	1, 16, 2, 133, 134, 135, 139	axtgbtwnid 28805	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141	140	olcd 888	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
142	132	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐺 ∈ TarskiG)
143	127	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ 𝑃)
144	111	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ∈ 𝑃)
145	126	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝑋 ∈ 𝑃)
146	128	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐴 ∈ 𝑃)
147		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝑋 ≠ 𝐶)
148	147	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ≠ 𝑋)
149	148	neneqd 2962	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → ¬ 𝐶 = 𝑋)
150	53	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ 𝑃)
151	106	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ≠ 𝐵)
152		simplr 781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
153	1, 2, 3, 132, 150, 127, 126, 151, 152	lncom 28967	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
154	77	necomd 3012	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
155	154	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ≠ 𝐶)
156	66	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
157	1, 2, 22, 150, 111, 127, 132, 3, 156	hlln 28950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
158	1, 2, 3, 132, 127, 111, 150, 155, 157	lncom 28967	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159	158	orcd 887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
160	1, 2, 3, 132, 126, 150, 127, 111, 153, 159	coltr 28993	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
161	1, 3, 2, 132, 127, 111, 126, 160	colrot1 28899	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162	161	orcomd 885	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163	162	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164	163	ord 878	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (¬ 𝐶 = 𝑋 → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165	149, 164	mpd 16	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
166	1, 3, 2, 132, 126, 128, 111, 115	btwncolg3 28897	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167	166	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168	1, 2, 3, 142, 143, 144, 145, 146, 165, 167	coltr 28993	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169	141, 168	pm2.61dane 3044	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170	1, 3, 2, 132, 126, 128, 127, 169	colrot2 28900	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
171	1, 3, 2, 132, 127, 126, 128, 170	colcom 28898	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172	171	orcomd 885	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 = 𝐵 ∨ 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173	172	ord 878	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (¬ 𝑋 = 𝐵 → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174	131, 173	mpd 16	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
175	1, 2, 22, 126, 127, 128, 129, 128, 3, 174	lnhl 28958	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴(𝐾‘𝐵)𝑋 ∨ 𝐵 ∈ (𝑋𝐼𝐴)))
176	99, 125, 175	mpjaodan 973	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
177	88, 176	pm2.61dane 3044	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
178	4	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐺 ∈ TarskiG)
179	8	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝑋 ∈ 𝑃)
180	12	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐵 ∈ 𝑃)
181	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ 𝑃)
182	6	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ 𝑃)
183		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐷 ∈ (𝐵𝐼𝐶))
184	1, 16, 2, 178, 179, 180, 68, 181, 182, 70, 183	axtgpasch 28806	. . . . 5 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185	184	adantr 486	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186		simplr 781	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ 𝑃)
187	181	ad3antrrr 743	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴 ∈ 𝑃)
188	180	ad3antrrr 743	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ∈ 𝑃)
189	178	ad3antrrr 743	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190		simprl 783	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
191	1, 16, 2, 189, 187, 186, 188, 190	tgbtwncom 28828	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
192	38	necomd 3012	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
193	192	ad4antr 745	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ≠ 𝐴)
194	189	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
195	6	ad5antr 747	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ 𝑃)
196	8	ad5antr 747	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋 ∈ 𝑃)
197	188	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
198		simp-4r 796	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199	106	necomd 3012	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐷)
200	199	ad5antr 747	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
201	200	neneqd 2962	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202		ioran 999	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203	198, 201, 202	sylanbrc 595	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
204	1, 3, 2, 194, 197, 195, 196, 203	ncolrot2 28903	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206	186	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ 𝑃)
207	1, 2, 3, 194, 195, 196, 197, 204	ncolne1 28970	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝑋)
208		simplrr 790	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
209	1, 2, 3, 194, 195, 196, 206, 207, 208	btwnlng1 28964	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210	205, 209	eqeltrrd 2863	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
211	1, 2, 3, 194, 195, 196, 207	tglinerflx1 28978	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212	106	ad5antr 747	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝐵)
213	212	necomd 3012	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
214	1, 2, 3, 194, 197, 195, 213	tglinerflx1 28978	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
215	1, 2, 3, 194, 197, 195, 213	tglinerflx2 28979	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
216	1, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215	tglineinteq 28991	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217	216, 201	pm2.65da 829	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218	217	neqned 2964	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ≠ 𝐵)
219	1, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218	btwnhl1 28955	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾‘𝐵)𝐴)
220	1, 2, 22, 186, 187, 188, 189, 219	hlcomd 28947	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾‘𝐵)𝑒)
221	178	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222	182	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷 ∈ 𝑃)
223		simplr 781	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ 𝑃)
224	179	ad3antrrr 743	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋 ∈ 𝑃)
225		simpr 490	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
226	1, 16, 2, 221, 222, 223, 224, 225	tgbtwncom 28828	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227	226	adantrl 729	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228	220, 227	jca 521	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
229	228	ex 418	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
230	229	reximdva 3177	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
231	185, 230	mpd 16	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
232	177, 231	pm2.61dan 825	. 2 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
233	76	simp3d 1162	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
234	52, 232, 233	mpjaodan 973	1 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∃wrex 3088 class class class wbr 5107 ‘cfv 6537 (class class class)co 7416 Basecbs 17305 distcds 17355 TarskiGcstrkg 28766 Itvcitv 28772 LineGclng 28773 hlGchlg 28940

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-oadd 8462 df-er 8699 df-map 8831 df-pm 8832 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-dju 9909 df-card 9947 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-nn 12261 df-2 12330 df-3 12331 df-n0 12532 df-xnn0 12605 df-z 12619 df-uz 12891 df-fz 13564 df-fzo 13712 df-hash 14397 df-word 14581 df-concat 14638 df-s1 14665 df-s2 14921 df-s3 14922 df-trkgc 28787 df-trkgb 28788 df-trkgcb 28789 df-trkgld 28791 df-trkg 28792 df-cgrg 28851 df-leg 28923 df-hlg 28941 df-mir 29002 df-rag 29046 df-perpg 29048

This theorem is used by: inaghl 29241

W3C validator