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 27021

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 2738	. . . 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 2738	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
17		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
18	1, 16, 2, 5, 13, 11, 7, 17	tgbtwncom 26753	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19		hlpasch.8	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))
20	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
21	1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20	outpasch 27020	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22		hlpasch.k	. . . . . . 7 ⊢ 𝐾 = (hlG‘𝐺)
23		simplr 765	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ 𝑃)
24	13	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵 ∈ 𝑃)
25	15	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ 𝑃)
26	5	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27		simprr 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
28	1, 16, 2, 26, 24, 25, 23, 27	tgbtwncom 26753	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝑒𝐼𝐵))
29	26	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
30	24	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
31	25	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ 𝑃)
32		simplrr 774	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝑒))
33		simpr 484	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
34	33	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
35	32, 34	eleqtrd 2841	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
36	1, 16, 2, 29, 30, 31, 35	axtgbtwnid 26731	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
37	36	eqcomd 2744	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38		hlpasch.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	38	ad3antrrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ≠ 𝐵)
40	39	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ≠ 𝐵)
41	40	neneqd 2947	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
42	37, 41	pm2.65da 813	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
43	42	neqned 2949	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ≠ 𝐵)
44	1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39	btwnhl2 26878	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾‘𝐵)𝑒)
45	7	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷 ∈ 𝑃)
46	9	ad2antrr 722	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋 ∈ 𝑃)
47		simprl 767	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
48	1, 16, 2, 26, 45, 23, 46, 47	tgbtwncom 26753	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
49	44, 48	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
50	49	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
51	50	reximdva 3202	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
52	21, 51	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
53	6	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃)
54	53	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ 𝑃)
55		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
56	55	breq2d 5082	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
57	55	eleq1d 2823	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
58	56, 57	anbi12d 630	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
59	14	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃)
60	59	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ 𝑃)
61	12	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵 ∈ 𝑃)
62	61	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵 ∈ 𝑃)
63	4	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
64	63	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65		hlpasch.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
66	1, 2, 22, 10, 6, 12, 4, 65	hlcomd 26869	. . . . . . . . 9 ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐶)
67	66	ad3antrrr 726	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
68	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶 ∈ 𝑃)
69	68	ad2antrr 722	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ∈ 𝑃)
70	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
71	70	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
73	72	oveq1d 7270	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
74	71, 73	eleqtrd 2841	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
75	1, 2, 22, 10, 6, 12, 4	ishlg 26867	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐷 ↔ (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
76	65, 75	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
77	76	simp1d 1140	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
78	77	ad3antrrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ≠ 𝐵)
79	38	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ≠ 𝐵)
80	79	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ≠ 𝐵)
81	1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80	hlbtwn 26876	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾‘𝐵)𝐶 ↔ 𝐷(𝐾‘𝐵)𝐴))
82	67, 81	mpbid 231	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐴)
83	1, 2, 22, 54, 60, 62, 64, 82	hlcomd 26869	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾‘𝐵)𝐷)
84	8	ad2antrr 722	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ 𝑃)
85	84	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 ∈ 𝑃)
86	1, 16, 2, 64, 85, 54	tgbtwntriv2 26752	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
87	83, 86	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
88	54, 58, 87	rspcedvd 3555	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
89	84	ad2antrr 722	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ 𝑃)
90		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
91	90	breq2d 5082	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝑋))
92	90	eleq1d 2823	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
93	91, 92	anbi12d 630	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
94	93	ad4ant14 748	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
95		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝐴(𝐾‘𝐵)𝑋)
96	1, 16, 2, 63, 84, 53	tgbtwntriv1 26756	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
97	96	ad2antrr 722	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
98	95, 97	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷)))
99	89, 94, 98	rspcedvd 3555	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
100	53	ad2antrr 722	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ 𝑃)
101		simpr 484	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102	101	breq2d 5082	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
103	101	eleq1d 2823	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104	102, 103	anbi12d 630	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
105	79	ad2antrr 722	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ≠ 𝐵)
106	1, 2, 22, 10, 6, 12, 4, 65	hlne2 26871	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐵)
107	106	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ≠ 𝐵)
108	63	ad2antrr 722	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
109	61	ad2antrr 722	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ 𝑃)
110	59	ad2antrr 722	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ 𝑃)
111	68	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐶 ∈ 𝑃)
112	111	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶 ∈ 𝑃)
113	84	ad2antrr 722	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋 ∈ 𝑃)
114		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
115	70	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116	115	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
117	1, 16, 2, 108, 113, 109, 110, 112, 114, 116	tgbtwnexch3 26759	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118		simp-4r 780	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
119	1, 2, 108, 109, 110, 100, 112, 117, 118	tgbtwnconn3 26842	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120	1, 2, 22, 14, 6, 12, 4	ishlg 26867	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121	120	ad4antr 728	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122	105, 107, 119, 121	mpbir3and 1340	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾‘𝐵)𝐷)
123	1, 16, 2, 108, 113, 100	tgbtwntriv2 26752	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124	122, 123	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
125	100, 104, 124	rspcedvd 3555	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
126	8	ad3antrrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ 𝑃)
127	12	ad3antrrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ∈ 𝑃)
128	14	ad3antrrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ 𝑃)
129	4	ad3antrrr 726	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
130		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ≠ 𝐵)
131	130	neneqd 2947	. . . . . . 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 7271	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139	136, 138	eleqtrrd 2842	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
140	1, 16, 2, 133, 134, 135, 139	axtgbtwnid 26731	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141	140	olcd 870	. . . . . . . . . . . 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 2998	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ≠ 𝑋)
149	148	neneqd 2947	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → ¬ 𝐶 = 𝑋)
150	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ 𝑃)
151	106	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ≠ 𝐵)
152		simplr 765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
153	1, 2, 3, 132, 150, 127, 126, 151, 152	lncom 26887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
154	77	necomd 2998	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
155	154	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ≠ 𝐶)
156	66	ad3antrrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
157	1, 2, 22, 150, 111, 127, 132, 3, 156	hlln 26872	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
158	1, 2, 3, 132, 127, 111, 150, 155, 157	lncom 26887	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159	158	orcd 869	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
160	1, 2, 3, 132, 126, 150, 127, 111, 153, 159	coltr 26912	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
161	1, 3, 2, 132, 127, 111, 126, 160	colrot1 26824	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162	161	orcomd 867	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164	163	ord 860	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (¬ 𝐶 = 𝑋 → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165	149, 164	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
166	1, 3, 2, 132, 126, 128, 111, 115	btwncolg3 26822	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167	166	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168	1, 2, 3, 142, 143, 144, 145, 146, 165, 167	coltr 26912	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169	141, 168	pm2.61dane 3031	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170	1, 3, 2, 132, 126, 128, 127, 169	colrot2 26825	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
171	1, 3, 2, 132, 127, 126, 128, 170	colcom 26823	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172	171	orcomd 867	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 = 𝐵 ∨ 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173	172	ord 860	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (¬ 𝑋 = 𝐵 → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174	131, 173	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
175	1, 2, 22, 126, 127, 128, 129, 128, 3, 174	lnhl 26880	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴(𝐾‘𝐵)𝑋 ∨ 𝐵 ∈ (𝑋𝐼𝐴)))
176	99, 125, 175	mpjaodan 955	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
177	88, 176	pm2.61dane 3031	. . 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 26732	. . . . 5 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185	184	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186		simplr 765	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ 𝑃)
187	181	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴 ∈ 𝑃)
188	180	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ∈ 𝑃)
189	178	ad3antrrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190		simprl 767	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
191	1, 16, 2, 189, 187, 186, 188, 190	tgbtwncom 26753	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
192	38	necomd 2998	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
193	192	ad4antr 728	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ≠ 𝐴)
194	189	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
195	6	ad5antr 730	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ 𝑃)
196	8	ad5antr 730	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋 ∈ 𝑃)
197	188	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
198		simp-4r 780	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199	106	necomd 2998	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐷)
200	199	ad5antr 730	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
201	200	neneqd 2947	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202		ioran 980	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203	198, 201, 202	sylanbrc 582	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
204	1, 3, 2, 194, 197, 195, 196, 203	ncolrot2 26828	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206	186	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ 𝑃)
207	1, 2, 3, 194, 195, 196, 197, 204	ncolne1 26890	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝑋)
208		simplrr 774	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
209	1, 2, 3, 194, 195, 196, 206, 207, 208	btwnlng1 26884	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210	205, 209	eqeltrrd 2840	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
211	1, 2, 3, 194, 195, 196, 207	tglinerflx1 26898	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212	106	ad5antr 730	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝐵)
213	212	necomd 2998	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
214	1, 2, 3, 194, 197, 195, 213	tglinerflx1 26898	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
215	1, 2, 3, 194, 197, 195, 213	tglinerflx2 26899	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
216	1, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215	tglineinteq 26910	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217	216, 201	pm2.65da 813	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218	217	neqned 2949	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ≠ 𝐵)
219	1, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218	btwnhl1 26877	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾‘𝐵)𝐴)
220	1, 2, 22, 186, 187, 188, 189, 219	hlcomd 26869	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾‘𝐵)𝑒)
221	178	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222	182	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷 ∈ 𝑃)
223		simplr 765	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ 𝑃)
224	179	ad3antrrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋 ∈ 𝑃)
225		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
226	1, 16, 2, 221, 222, 223, 224, 225	tgbtwncom 26753	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227	226	adantrl 712	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228	220, 227	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
229	228	ex 412	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
230	229	reximdva 3202	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
231	185, 230	mpd 15	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
232	177, 231	pm2.61dan 809	. 2 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
233	76	simp3d 1142	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
234	52, 232, 233	mpjaodan 955	1 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 class class class wbr 5070 ‘cfv 6418 (class class class)co 7255 Basecbs 16840 distcds 16897 TarskiGcstrkg 26693 Itvcitv 26699 LineGclng 26700 hlGchlg 26865

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-fz 13169 df-fzo 13312 df-hash 13973 df-word 14146 df-concat 14202 df-s1 14229 df-s2 14489 df-s3 14490 df-trkgc 26713 df-trkgb 26714 df-trkgcb 26715 df-trkgld 26717 df-trkg 26718 df-cgrg 26776 df-leg 26848 df-hlg 26866 df-mir 26918 df-rag 26959 df-perpg 26961

This theorem is referenced by: inaghl 27110

W3C validator