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 28727

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 2730	. . . 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 2730	. . . . 5 ⊢ (dist‘𝐺) = (dist‘𝐺)
17		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐵𝐼𝐷))
18	1, 16, 2, 5, 13, 11, 7, 17	tgbtwncom 28459	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐶 ∈ (𝐷𝐼𝐵))
19		hlpasch.8	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ (𝑋𝐼𝐶))
20	19	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → 𝐴 ∈ (𝑋𝐼𝐶))
21	1, 2, 3, 5, 7, 9, 11, 13, 15, 18, 20	outpasch 28726	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)))
22		hlpasch.k	. . . . . . 7 ⊢ 𝐾 = (hlG‘𝐺)
23		simplr 768	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ 𝑃)
24	13	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐵 ∈ 𝑃)
25	15	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ 𝑃)
26	5	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐺 ∈ TarskiG)
27		simprr 772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ∈ (𝐵𝐼𝑒))
28	1, 16, 2, 26, 24, 25, 23, 27	tgbtwncom 28459	. . . . . . 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 7357	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → (𝐵𝐼𝑒) = (𝐵𝐼𝐵))
35	32, 34	eleqtrd 2831	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐵))
36	1, 16, 2, 29, 30, 31, 35	axtgbtwnid 28437	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐴)
37	36	eqcomd 2736	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 = 𝐵)
38		hlpasch.6	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
39	38	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴 ≠ 𝐵)
40	39	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → 𝐴 ≠ 𝐵)
41	40	neneqd 2931	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) ∧ 𝑒 = 𝐵) → ¬ 𝐴 = 𝐵)
42	37, 41	pm2.65da 816	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → ¬ 𝑒 = 𝐵)
43	42	neqned 2933	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ≠ 𝐵)
44	1, 2, 22, 23, 24, 25, 26, 25, 28, 43, 39	btwnhl2 28584	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐴(𝐾‘𝐵)𝑒)
45	7	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝐷 ∈ 𝑃)
46	9	ad2antrr 726	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑋 ∈ 𝑃)
47		simprl 770	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝐷𝐼𝑋))
48	1, 16, 2, 26, 45, 23, 46, 47	tgbtwncom 28459	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → 𝑒 ∈ (𝑋𝐼𝐷))
49	44, 48	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
50	49	ex 412	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
51	50	reximdva 3143	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐷𝐼𝑋) ∧ 𝐴 ∈ (𝐵𝐼𝑒)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
52	21, 51	mpd 15	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ (𝐵𝐼𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
53	6	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐷 ∈ 𝑃)
54	53	adantr 480	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ 𝑃)
55		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
56	55	breq2d 5101	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
57	55	eleq1d 2814	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
58	56, 57	anbi12d 632	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
59	14	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ∈ 𝑃)
60	59	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ 𝑃)
61	12	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐵 ∈ 𝑃)
62	61	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐵 ∈ 𝑃)
63	4	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐺 ∈ TarskiG)
64	63	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐺 ∈ TarskiG)
65		hlpasch.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶(𝐾‘𝐵)𝐷)
66	1, 2, 22, 10, 6, 12, 4, 65	hlcomd 28575	. . . . . . . . 9 ⊢ (𝜑 → 𝐷(𝐾‘𝐵)𝐶)
67	66	ad3antrrr 730	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
68	10	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐶 ∈ 𝑃)
69	68	ad2antrr 726	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ∈ 𝑃)
70	19	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → 𝐴 ∈ (𝑋𝐼𝐶))
71	70	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
72		simpr 484	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 = 𝐵)
73	72	oveq1d 7356	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝑋𝐼𝐶) = (𝐵𝐼𝐶))
74	71, 73	eleqtrd 2831	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ∈ (𝐵𝐼𝐶))
75	1, 2, 22, 10, 6, 12, 4	ishlg 28573	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶(𝐾‘𝐵)𝐷 ↔ (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))))
76	65, 75	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶))))
77	76	simp1d 1142	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ≠ 𝐵)
78	77	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐶 ≠ 𝐵)
79	38	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝐴 ≠ 𝐵)
80	79	adantr 480	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴 ≠ 𝐵)
81	1, 2, 22, 54, 69, 62, 64, 60, 74, 78, 80	hlbtwn 28582	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐷(𝐾‘𝐵)𝐶 ↔ 𝐷(𝐾‘𝐵)𝐴))
82	67, 81	mpbid 232	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷(𝐾‘𝐵)𝐴)
83	1, 2, 22, 54, 60, 62, 64, 82	hlcomd 28575	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐴(𝐾‘𝐵)𝐷)
84	8	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ 𝑃)
85	84	adantr 480	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝑋 ∈ 𝑃)
86	1, 16, 2, 64, 85, 54	tgbtwntriv2 28458	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → 𝐷 ∈ (𝑋𝐼𝐷))
87	83, 86	jca 511	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
88	54, 58, 87	rspcedvd 3577	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 = 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
89	84	ad2antrr 726	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ 𝑃)
90		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → 𝑒 = 𝑋)
91	90	breq2d 5101	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝑋))
92	90	eleq1d 2814	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝑋 ∈ (𝑋𝐼𝐷)))
93	91, 92	anbi12d 632	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
94	93	ad4ant14 752	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) ∧ 𝑒 = 𝑋) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷))))
95		simpr 484	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝐴(𝐾‘𝐵)𝑋)
96	1, 16, 2, 63, 84, 53	tgbtwntriv1 28462	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → 𝑋 ∈ (𝑋𝐼𝐷))
97	96	ad2antrr 726	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → 𝑋 ∈ (𝑋𝐼𝐷))
98	95, 97	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → (𝐴(𝐾‘𝐵)𝑋 ∧ 𝑋 ∈ (𝑋𝐼𝐷)))
99	89, 94, 98	rspcedvd 3577	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐴(𝐾‘𝐵)𝑋) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
100	53	ad2antrr 726	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ 𝑃)
101		simpr 484	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → 𝑒 = 𝐷)
102	101	breq2d 5101	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝐴(𝐾‘𝐵)𝑒 ↔ 𝐴(𝐾‘𝐵)𝐷))
103	101	eleq1d 2814	. . . . . . 7 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → (𝑒 ∈ (𝑋𝐼𝐷) ↔ 𝐷 ∈ (𝑋𝐼𝐷)))
104	102, 103	anbi12d 632	. . . . . 6 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) ∧ 𝑒 = 𝐷) → ((𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)) ↔ (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷))))
105	79	ad2antrr 726	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ≠ 𝐵)
106	1, 2, 22, 10, 6, 12, 4, 65	hlne2 28577	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ≠ 𝐵)
107	106	ad4antr 732	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ≠ 𝐵)
108	63	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐺 ∈ TarskiG)
109	61	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ 𝑃)
110	59	ad2antrr 726	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ 𝑃)
111	68	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐶 ∈ 𝑃)
112	111	adantr 480	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐶 ∈ 𝑃)
113	84	ad2antrr 726	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝑋 ∈ 𝑃)
114		simpr 484	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐵 ∈ (𝑋𝐼𝐴))
115	70	ad2antrr 726	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋𝐼𝐶))
116	115	adantr 480	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝑋𝐼𝐶))
117	1, 16, 2, 108, 113, 109, 110, 112, 114, 116	tgbtwnexch3 28465	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴 ∈ (𝐵𝐼𝐶))
118		simp-4r 783	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝐵𝐼𝐶))
119	1, 2, 108, 109, 110, 100, 112, 117, 118	tgbtwnconn3 28548	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))
120	1, 2, 22, 14, 6, 12, 4	ishlg 28573	. . . . . . . . 9 ⊢ (𝜑 → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
121	120	ad4antr 732	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ↔ (𝐴 ≠ 𝐵 ∧ 𝐷 ≠ 𝐵 ∧ (𝐴 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐴)))))
122	105, 107, 119, 121	mpbir3and 1343	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐴(𝐾‘𝐵)𝐷)
123	1, 16, 2, 108, 113, 100	tgbtwntriv2 28458	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → 𝐷 ∈ (𝑋𝐼𝐷))
124	122, 123	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → (𝐴(𝐾‘𝐵)𝐷 ∧ 𝐷 ∈ (𝑋𝐼𝐷)))
125	100, 104, 124	rspcedvd 3577	. . . . 5 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝐵 ∈ (𝑋𝐼𝐴)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
126	8	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ 𝑃)
127	12	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ∈ 𝑃)
128	14	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ 𝑃)
129	4	ad3antrrr 730	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐺 ∈ TarskiG)
130		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ≠ 𝐵)
131	130	neneqd 2931	. . . . . . 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 7357	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → (𝑋𝐼𝑋) = (𝑋𝐼𝐶))
139	136, 138	eleqtrrd 2832	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝐴 ∈ (𝑋𝐼𝑋))
140	1, 16, 2, 133, 134, 135, 139	axtgbtwnid 28437	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 = 𝐶) → 𝑋 = 𝐴)
141	140	olcd 874	. . . . . . . . . . . 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 2981	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐶 ≠ 𝑋)
149	148	neneqd 2931	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → ¬ 𝐶 = 𝑋)
150	53	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ 𝑃)
151	106	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ≠ 𝐵)
152		simplr 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
153	1, 2, 3, 132, 150, 127, 126, 151, 152	lncom 28593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝑋 ∈ (𝐷(LineG‘𝐺)𝐵))
154	77	necomd 2981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐵 ≠ 𝐶)
155	154	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐵 ≠ 𝐶)
156	66	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷(𝐾‘𝐵)𝐶)
157	1, 2, 22, 150, 111, 127, 132, 3, 156	hlln 28578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐶(LineG‘𝐺)𝐵))
158	1, 2, 3, 132, 127, 111, 150, 155, 157	lncom 28593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐶))
159	158	orcd 873	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐷 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
160	1, 2, 3, 132, 126, 150, 127, 111, 153, 159	coltr 28618	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 ∈ (𝐵(LineG‘𝐺)𝐶) ∨ 𝐵 = 𝐶))
161	1, 3, 2, 132, 127, 111, 126, 160	colrot1 28530	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝐶(LineG‘𝐺)𝑋) ∨ 𝐶 = 𝑋))
162	161	orcomd 871	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
163	162	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 = 𝑋 ∨ 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
164	163	ord 864	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (¬ 𝐶 = 𝑋 → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋)))
165	149, 164	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → 𝐵 ∈ (𝐶(LineG‘𝐺)𝑋))
166	1, 3, 2, 132, 126, 128, 111, 115	btwncolg3 28528	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
167	166	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐶 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
168	1, 2, 3, 142, 143, 144, 145, 146, 165, 167	coltr 28618	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) ∧ 𝑋 ≠ 𝐶) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
169	141, 168	pm2.61dane 3013	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐵 ∈ (𝑋(LineG‘𝐺)𝐴) ∨ 𝑋 = 𝐴))
170	1, 3, 2, 132, 126, 128, 127, 169	colrot2 28531	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝐵(LineG‘𝐺)𝑋) ∨ 𝐵 = 𝑋))
171	1, 3, 2, 132, 127, 126, 128, 170	colcom 28529	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
172	171	orcomd 871	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝑋 = 𝐵 ∨ 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
173	172	ord 864	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (¬ 𝑋 = 𝐵 → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵)))
174	131, 173	mpd 15	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → 𝐴 ∈ (𝑋(LineG‘𝐺)𝐵))
175	1, 2, 22, 126, 127, 128, 129, 128, 3, 174	lnhl 28586	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → (𝐴(𝐾‘𝐵)𝑋 ∨ 𝐵 ∈ (𝑋𝐼𝐴)))
176	99, 125, 175	mpjaodan 960	. . . 4 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑋 ≠ 𝐵) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
177	88, 176	pm2.61dane 3013	. . 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 28438	. . . . 5 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
185	184	adantr 480	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)))
186		simplr 768	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ 𝑃)
187	181	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴 ∈ 𝑃)
188	180	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ∈ 𝑃)
189	178	ad3antrrr 730	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐺 ∈ TarskiG)
190		simprl 770	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐴𝐼𝐵))
191	1, 16, 2, 189, 187, 186, 188, 190	tgbtwncom 28459	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝐵𝐼𝐴))
192	38	necomd 2981	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
193	192	ad4antr 732	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐵 ≠ 𝐴)
194	189	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐺 ∈ TarskiG)
195	6	ad5antr 734	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ 𝑃)
196	8	ad5antr 734	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑋 ∈ 𝑃)
197	188	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ 𝑃)
198		simp-4r 783	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷))
199	106	necomd 2981	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 ≠ 𝐷)
200	199	ad5antr 734	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
201	200	neneqd 2931	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ 𝐵 = 𝐷)
202		ioran 985	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷) ↔ (¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∧ ¬ 𝐵 = 𝐷))
203	198, 201, 202	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝑋 ∈ (𝐵(LineG‘𝐺)𝐷) ∨ 𝐵 = 𝐷))
204	1, 3, 2, 194, 197, 195, 196, 203	ncolrot2 28534	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → ¬ (𝐷 ∈ (𝑋(LineG‘𝐺)𝐵) ∨ 𝑋 = 𝐵))
205		simpr 484	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 = 𝐵)
206	186	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ 𝑃)
207	1, 2, 3, 194, 195, 196, 197, 204	ncolne1 28596	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝑋)
208		simplrr 777	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷𝐼𝑋))
209	1, 2, 3, 194, 195, 196, 206, 207, 208	btwnlng1 28590	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝑒 ∈ (𝐷(LineG‘𝐺)𝑋))
210	205, 209	eqeltrrd 2830	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐷(LineG‘𝐺)𝑋))
211	1, 2, 3, 194, 195, 196, 207	tglinerflx1 28604	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐷(LineG‘𝐺)𝑋))
212	106	ad5antr 734	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ≠ 𝐵)
213	212	necomd 2981	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ≠ 𝐷)
214	1, 2, 3, 194, 197, 195, 213	tglinerflx1 28604	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 ∈ (𝐵(LineG‘𝐺)𝐷))
215	1, 2, 3, 194, 197, 195, 213	tglinerflx2 28605	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐷 ∈ (𝐵(LineG‘𝐺)𝐷))
216	1, 2, 3, 194, 195, 196, 197, 195, 204, 210, 211, 214, 215	tglineinteq 28616	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) ∧ 𝑒 = 𝐵) → 𝐵 = 𝐷)
217	216, 201	pm2.65da 816	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → ¬ 𝑒 = 𝐵)
218	217	neqned 2933	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ≠ 𝐵)
219	1, 2, 22, 188, 187, 186, 189, 187, 191, 193, 218	btwnhl1 28583	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒(𝐾‘𝐵)𝐴)
220	1, 2, 22, 186, 187, 188, 189, 219	hlcomd 28575	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝐴(𝐾‘𝐵)𝑒)
221	178	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐺 ∈ TarskiG)
222	182	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝐷 ∈ 𝑃)
223		simplr 768	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ 𝑃)
224	179	ad3antrrr 730	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑋 ∈ 𝑃)
225		simpr 484	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝐷𝐼𝑋))
226	1, 16, 2, 221, 222, 223, 224, 225	tgbtwncom 28459	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → 𝑒 ∈ (𝑋𝐼𝐷))
227	226	adantrl 716	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → 𝑒 ∈ (𝑋𝐼𝐷))
228	220, 227	jca 511	. . . . . 6 ⊢ (((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) ∧ (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋))) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
229	228	ex 412	. . . . 5 ⊢ ((((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) ∧ 𝑒 ∈ 𝑃) → ((𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
230	229	reximdva 3143	. . . 4 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → (∃𝑒 ∈ 𝑃 (𝑒 ∈ (𝐴𝐼𝐵) ∧ 𝑒 ∈ (𝐷𝐼𝑋)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷))))
231	185, 230	mpd 15	. . 3 ⊢ (((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) ∧ ¬ 𝑋 ∈ (𝐵(LineG‘𝐺)𝐷)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
232	177, 231	pm2.61dan 812	. 2 ⊢ ((𝜑 ∧ 𝐷 ∈ (𝐵𝐼𝐶)) → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))
233	76	simp3d 1144	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐵𝐼𝐷) ∨ 𝐷 ∈ (𝐵𝐼𝐶)))
234	52, 232, 233	mpjaodan 960	1 ⊢ (𝜑 → ∃𝑒 ∈ 𝑃 (𝐴(𝐾‘𝐵)𝑒 ∧ 𝑒 ∈ (𝑋𝐼𝐷)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ∃wrex 3054 class class class wbr 5089 ‘cfv 6477 (class class class)co 7341 Basecbs 17112 distcds 17162 TarskiGcstrkg 28398 Itvcitv 28404 LineGclng 28405 hlGchlg 28571

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-tp 4579 df-op 4581 df-uni 4858 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-om 7792 df-1st 7916 df-2nd 7917 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-oadd 8384 df-er 8617 df-map 8747 df-pm 8748 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-dju 9786 df-card 9824 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-nn 12118 df-2 12180 df-3 12181 df-n0 12374 df-xnn0 12447 df-z 12461 df-uz 12725 df-fz 13400 df-fzo 13547 df-hash 14230 df-word 14413 df-concat 14470 df-s1 14496 df-s2 14747 df-s3 14748 df-trkgc 28419 df-trkgb 28420 df-trkgcb 28421 df-trkgld 28423 df-trkg 28424 df-cgrg 28482 df-leg 28554 df-hlg 28572 df-mir 28624 df-rag 28665 df-perpg 28667

This theorem is referenced by: inaghl 28816

W3C validator