hlpasch

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

	Ref	Expression
Hypotheses	hlpasch.p	$⊢ P = {Base}_{G}$
	hlpasch.i	$⊢ I = Itv (G)$
	hlpasch.k	$⊢ K = {hl}_{𝒢} (G)$
	hlpasch.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	hlpasch.1	$⊢ φ \to A \in P$
	hlpasch.2	$⊢ φ \to B \in P$
	hlpasch.3	$⊢ φ \to C \in P$
	hlpasch.4	$⊢ φ \to X \in P$
	hlpasch.5	$⊢ φ \to D \in P$
	hlpasch.6	$⊢ φ \to A \neq B$
	hlpasch.7	$⊢ φ \to C K (B) D$
	hlpasch.8	$⊢ φ \to A \in (X I C)$
Assertion	hlpasch	$⊢ φ \to \exists e \in P (A K (B) e \land e \in (X I D))$

Proof

Step	Hyp	Ref	Expression
1		hlpasch.p	$⊢ P = {Base}_{G}$
2		hlpasch.i	$⊢ I = Itv (G)$
3		hlpasch.k	$⊢ K = {hl}_{𝒢} (G)$
4		hlpasch.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		hlpasch.1	$⊢ φ \to A \in P$
6		hlpasch.2	$⊢ φ \to B \in P$
7		hlpasch.3	$⊢ φ \to C \in P$
8		hlpasch.4	$⊢ φ \to X \in P$
9		hlpasch.5	$⊢ φ \to D \in P$
10		hlpasch.6	$⊢ φ \to A \neq B$
11		hlpasch.7	$⊢ φ \to C K (B) D$
12		hlpasch.8	$⊢ φ \to A \in (X I C)$
13		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
14	4	adantr	$⊢ (φ \land C \in (B I D)) \to G \in 𝒢_{Tarski}$
15	9	adantr	$⊢ (φ \land C \in (B I D)) \to D \in P$
16	8	adantr	$⊢ (φ \land C \in (B I D)) \to X \in P$
17	7	adantr	$⊢ (φ \land C \in (B I D)) \to C \in P$
18	6	adantr	$⊢ (φ \land C \in (B I D)) \to B \in P$
19	5	adantr	$⊢ (φ \land C \in (B I D)) \to A \in P$
20		eqid	$⊢ dist (G) = dist (G)$
21		simpr	$⊢ (φ \land C \in (B I D)) \to C \in (B I D)$
22	1 20 2 14 18 17 15 21	tgbtwncom	$⊢ (φ \land C \in (B I D)) \to C \in (D I B)$
23	12	adantr	$⊢ (φ \land C \in (B I D)) \to A \in (X I C)$
24	1 2 13 14 15 16 17 18 19 22 23	outpasch	$⊢ (φ \land C \in (B I D)) \to \exists e \in P (e \in (D I X) \land A \in (B I e))$
25		simplr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to e \in P$
26	18	ad2antrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to B \in P$
27	19	ad2antrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to A \in P$
28	14	ad2antrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to G \in 𝒢_{Tarski}$
29		simprr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to A \in (B I e)$
30	1 20 2 28 26 27 25 29	tgbtwncom	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to A \in (e I B)$
31	28	adantr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to G \in 𝒢_{Tarski}$
32	26	adantr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to B \in P$
33	27	adantr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to A \in P$
34		simplrr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to A \in (B I e)$
35		simpr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to e = B$
36	35	oveq2d	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to B I e = B I B$
37	34 36	eleqtrd	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to A \in (B I B)$
38	1 20 2 31 32 33 37	axtgbtwnid	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to B = A$
39	38	eqcomd	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to A = B$
40	10	ad3antrrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to A \neq B$
41	40	adantr	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to A \neq B$
42	41	neneqd	$⊢ ((((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \land e = B) \to \neg A = B$
43	39 42	pm2.65da	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to \neg e = B$
44	43	neqned	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to e \neq B$
45	1 2 3 25 26 27 28 27 30 44 40	btwnhl2	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to A K (B) e$
46	15	ad2antrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to D \in P$
47	16	ad2antrr	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to X \in P$
48		simprl	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to e \in (D I X)$
49	1 20 2 28 46 25 47 48	tgbtwncom	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to e \in (X I D)$
50	45 49	jca	$⊢ (((φ \land C \in (B I D)) \land e \in P) \land (e \in (D I X) \land A \in (B I e))) \to (A K (B) e \land e \in (X I D))$
51	50	ex	$⊢ ((φ \land C \in (B I D)) \land e \in P) \to ((e \in (D I X) \land A \in (B I e)) \to (A K (B) e \land e \in (X I D)))$
52	51	reximdva	$⊢ (φ \land C \in (B I D)) \to (\exists e \in P (e \in (D I X) \land A \in (B I e)) \to \exists e \in P (A K (B) e \land e \in (X I D)))$
53	24 52	mpd	$⊢ (φ \land C \in (B I D)) \to \exists e \in P (A K (B) e \land e \in (X I D))$
54	9	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to D \in P$
55	54	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to D \in P$
56		simpr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \land e = D) \to e = D$
57	56	breq2d	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \land e = D) \to (A K (B) e \leftrightarrow A K (B) D)$
58	56	eleq1d	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \land e = D) \to (e \in (X I D) \leftrightarrow D \in (X I D))$
59	57 58	anbi12d	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \land e = D) \to ((A K (B) e \land e \in (X I D)) \leftrightarrow (A K (B) D \land D \in (X I D)))$
60	5	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to A \in P$
61	60	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to A \in P$
62	6	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to B \in P$
63	62	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to B \in P$
64	4	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to G \in 𝒢_{Tarski}$
65	64	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to G \in 𝒢_{Tarski}$
66	1 2 3 7 9 6 4 11	hlcomd	$⊢ φ \to D K (B) C$
67	66	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to D K (B) C$
68	7	adantr	$⊢ (φ \land D \in (B I C)) \to C \in P$
69	68	ad2antrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to C \in P$
70	12	adantr	$⊢ (φ \land D \in (B I C)) \to A \in (X I C)$
71	70	ad2antrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to A \in (X I C)$
72		simpr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to X = B$
73	72	oveq1d	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to X I C = B I C$
74	71 73	eleqtrd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to A \in (B I C)$
75	1 2 3 7 9 6 4	ishlg	$⊢ φ \to (C K (B) D \leftrightarrow (C \neq B \land D \neq B \land (C \in (B I D) \lor D \in (B I C))))$
76	11 75	mpbid	$⊢ φ \to (C \neq B \land D \neq B \land (C \in (B I D) \lor D \in (B I C)))$
77	76	simp1d	$⊢ φ \to C \neq B$
78	77	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to C \neq B$
79	10	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to A \neq B$
80	79	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to A \neq B$
81	1 2 3 55 69 63 65 61 74 78 80	hlbtwn	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to (D K (B) C \leftrightarrow D K (B) A)$
82	67 81	mpbid	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to D K (B) A$
83	1 2 3 55 61 63 65 82	hlcomd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to A K (B) D$
84	8	ad2antrr	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to X \in P$
85	84	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to X \in P$
86	1 20 2 65 85 55	tgbtwntriv2	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to D \in (X I D)$
87	83 86	jca	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to (A K (B) D \land D \in (X I D))$
88	55 59 87	rspcedvd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X = B) \to \exists e \in P (A K (B) e \land e \in (X I D))$
89	84	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \to X \in P$
90		simpr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land e = X) \to e = X$
91	90	breq2d	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land e = X) \to (A K (B) e \leftrightarrow A K (B) X)$
92	90	eleq1d	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land e = X) \to (e \in (X I D) \leftrightarrow X \in (X I D))$
93	91 92	anbi12d	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land e = X) \to ((A K (B) e \land e \in (X I D)) \leftrightarrow (A K (B) X \land X \in (X I D)))$
94	93	ad4ant14	$⊢ (((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \land e = X) \to ((A K (B) e \land e \in (X I D)) \leftrightarrow (A K (B) X \land X \in (X I D)))$
95		simpr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \to A K (B) X$
96	1 20 2 64 84 54	tgbtwntriv1	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to X \in (X I D)$
97	96	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \to X \in (X I D)$
98	95 97	jca	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \to (A K (B) X \land X \in (X I D))$
99	89 94 98	rspcedvd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land A K (B) X) \to \exists e \in P (A K (B) e \land e \in (X I D))$
100	54	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to D \in P$
101		simpr	$⊢ (((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \land e = D) \to e = D$
102	101	breq2d	$⊢ (((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \land e = D) \to (A K (B) e \leftrightarrow A K (B) D)$
103	101	eleq1d	$⊢ (((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \land e = D) \to (e \in (X I D) \leftrightarrow D \in (X I D))$
104	102 103	anbi12d	$⊢ (((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \land e = D) \to ((A K (B) e \land e \in (X I D)) \leftrightarrow (A K (B) D \land D \in (X I D)))$
105	79	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to A \neq B$
106	1 2 3 7 9 6 4 11	hlne2	$⊢ φ \to D \neq B$
107	106	ad4antr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to D \neq B$
108	64	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to G \in 𝒢_{Tarski}$
109	62	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to B \in P$
110	60	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to A \in P$
111	68	ad2antrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to C \in P$
112	111	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to C \in P$
113	84	ad2antrr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to X \in P$
114		simpr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to B \in (X I A)$
115	70	ad2antrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to A \in (X I C)$
116	115	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to A \in (X I C)$
117	1 20 2 108 113 109 110 112 114 116	tgbtwnexch3	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to A \in (B I C)$
118		simp-4r	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to D \in (B I C)$
119	1 2 108 109 110 100 112 117 118	tgbtwnconn3	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to (A \in (B I D) \lor D \in (B I A))$
120	1 2 3 5 9 6 4	ishlg	$⊢ φ \to (A K (B) D \leftrightarrow (A \neq B \land D \neq B \land (A \in (B I D) \lor D \in (B I A))))$
121	120	ad4antr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to (A K (B) D \leftrightarrow (A \neq B \land D \neq B \land (A \in (B I D) \lor D \in (B I A))))$
122	105 107 119 121	mpbir3and	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to A K (B) D$
123	1 20 2 108 113 100	tgbtwntriv2	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to D \in (X I D)$
124	122 123	jca	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to (A K (B) D \land D \in (X I D))$
125	100 104 124	rspcedvd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land B \in (X I A)) \to \exists e \in P (A K (B) e \land e \in (X I D))$
126	8	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to X \in P$
127	6	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to B \in P$
128	5	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to A \in P$
129	4	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to G \in 𝒢_{Tarski}$
130		simpr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to X \neq B$
131	130	neneqd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to \neg X = B$
132	64	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to G \in 𝒢_{Tarski}$
133	132	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to G \in 𝒢_{Tarski}$
134	126	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to X \in P$
135	128	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to A \in P$
136	115	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to A \in (X I C)$
137		simpr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to X = C$
138	137	oveq2d	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to X I X = X I C$
139	136 138	eleqtrrd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to A \in (X I X)$
140	1 20 2 133 134 135 139	axtgbtwnid	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to X = A$
141	140	olcd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X = C) \to (B \in (X {Line}_{𝒢} (G) A) \lor X = A)$
142	132	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to G \in 𝒢_{Tarski}$
143	127	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to B \in P$
144	111	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to C \in P$
145	126	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to X \in P$
146	128	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to A \in P$
147		simpr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to X \neq C$
148	147	necomd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to C \neq X$
149	148	neneqd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to \neg C = X$
150	54	adantr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to D \in P$
151	106	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to D \neq B$
152		simplr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to X \in (B {Line}_{𝒢} (G) D)$
153	1 2 13 132 150 127 126 151 152	lncom	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to X \in (D {Line}_{𝒢} (G) B)$
154	77	necomd	$⊢ φ \to B \neq C$
155	154	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to B \neq C$
156	66	ad3antrrr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to D K (B) C$
157	1 2 3 150 111 127 132 13 156	hlln	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to D \in (C {Line}_{𝒢} (G) B)$
158	1 2 13 132 127 111 150 155 157	lncom	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to D \in (B {Line}_{𝒢} (G) C)$
159	158	orcd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (D \in (B {Line}_{𝒢} (G) C) \lor B = C)$
160	1 2 13 132 126 150 127 111 153 159	coltr	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (X \in (B {Line}_{𝒢} (G) C) \lor B = C)$
161	1 13 2 132 127 111 126 160	colrot1	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (B \in (C {Line}_{𝒢} (G) X) \lor C = X)$
162	161	orcomd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (C = X \lor B \in (C {Line}_{𝒢} (G) X))$
163	162	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to (C = X \lor B \in (C {Line}_{𝒢} (G) X))$
164	163	ord	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to (\neg C = X \to B \in (C {Line}_{𝒢} (G) X))$
165	149 164	mpd	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to B \in (C {Line}_{𝒢} (G) X)$
166	1 13 2 132 126 128 111 115	btwncolg3	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (C \in (X {Line}_{𝒢} (G) A) \lor X = A)$
167	166	adantr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to (C \in (X {Line}_{𝒢} (G) A) \lor X = A)$
168	1 2 13 142 143 144 145 146 165 167	coltr	$⊢ ((((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \land X \neq C) \to (B \in (X {Line}_{𝒢} (G) A) \lor X = A)$
169	141 168	pm2.61dane	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (B \in (X {Line}_{𝒢} (G) A) \lor X = A)$
170	1 13 2 132 126 128 127 169	colrot2	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (A \in (B {Line}_{𝒢} (G) X) \lor B = X)$
171	1 13 2 132 127 126 128 170	colcom	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (A \in (X {Line}_{𝒢} (G) B) \lor X = B)$
172	171	orcomd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (X = B \lor A \in (X {Line}_{𝒢} (G) B))$
173	172	ord	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (\neg X = B \to A \in (X {Line}_{𝒢} (G) B))$
174	131 173	mpd	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to A \in (X {Line}_{𝒢} (G) B)$
175	1 2 3 126 127 128 129 128 13 174	lnhl	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to (A K (B) X \lor B \in (X I A))$
176	99 125 175	mpjaodan	$⊢ (((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \land X \neq B) \to \exists e \in P (A K (B) e \land e \in (X I D))$
177	88 176	pm2.61dane	$⊢ ((φ \land D \in (B I C)) \land X \in (B {Line}_{𝒢} (G) D)) \to \exists e \in P (A K (B) e \land e \in (X I D))$
178	4	adantr	$⊢ (φ \land D \in (B I C)) \to G \in 𝒢_{Tarski}$
179	8	adantr	$⊢ (φ \land D \in (B I C)) \to X \in P$
180	6	adantr	$⊢ (φ \land D \in (B I C)) \to B \in P$
181	5	adantr	$⊢ (φ \land D \in (B I C)) \to A \in P$
182	9	adantr	$⊢ (φ \land D \in (B I C)) \to D \in P$
183		simpr	$⊢ (φ \land D \in (B I C)) \to D \in (B I C)$
184	1 20 2 178 179 180 68 181 182 70 183	axtgpasch	$⊢ (φ \land D \in (B I C)) \to \exists e \in P (e \in (A I B) \land e \in (D I X))$
185	184	adantr	$⊢ ((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \to \exists e \in P (e \in (A I B) \land e \in (D I X))$
186		simplr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e \in P$
187	181	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to A \in P$
188	180	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to B \in P$
189	178	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to G \in 𝒢_{Tarski}$
190		simprl	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e \in (A I B)$
191	1 20 2 189 187 186 188 190	tgbtwncom	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e \in (B I A)$
192	10	necomd	$⊢ φ \to B \neq A$
193	192	ad4antr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to B \neq A$
194	189	adantr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to G \in 𝒢_{Tarski}$
195	9	ad5antr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to D \in P$
196	8	ad5antr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to X \in P$
197	188	adantr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B \in P$
198		simp-4r	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to \neg X \in (B {Line}_{𝒢} (G) D)$
199	106	necomd	$⊢ φ \to B \neq D$
200	199	ad5antr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B \neq D$
201	200	neneqd	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to \neg B = D$
202		ioran	$⊢ \neg (X \in (B {Line}_{𝒢} (G) D) \lor B = D) \leftrightarrow (\neg X \in (B {Line}_{𝒢} (G) D) \land \neg B = D)$
203	198 201 202	sylanbrc	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to \neg (X \in (B {Line}_{𝒢} (G) D) \lor B = D)$
204	1 13 2 194 197 195 196 203	ncolrot2	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to \neg (D \in (X {Line}_{𝒢} (G) B) \lor X = B)$
205		simpr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to e = B$
206	186	adantr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to e \in P$
207	1 2 13 194 195 196 197 204	ncolne1	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to D \neq X$
208		simplrr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to e \in (D I X)$
209	1 2 13 194 195 196 206 207 208	btwnlng1	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to e \in (D {Line}_{𝒢} (G) X)$
210	205 209	eqeltrrd	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B \in (D {Line}_{𝒢} (G) X)$
211	1 2 13 194 195 196 207	tglinerflx1	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to D \in (D {Line}_{𝒢} (G) X)$
212	106	ad5antr	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to D \neq B$
213	212	necomd	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B \neq D$
214	1 2 13 194 197 195 213	tglinerflx1	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B \in (B {Line}_{𝒢} (G) D)$
215	1 2 13 194 197 195 213	tglinerflx2	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to D \in (B {Line}_{𝒢} (G) D)$
216	1 2 13 194 195 196 197 195 204 210 211 214 215	tglineinteq	$⊢ (((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \land e = B) \to B = D$
217	216 201	pm2.65da	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to \neg e = B$
218	217	neqned	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e \neq B$
219	1 2 3 188 187 186 189 187 191 193 218	btwnhl1	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e K (B) A$
220	1 2 3 186 187 188 189 219	hlcomd	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to A K (B) e$
221	178	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to G \in 𝒢_{Tarski}$
222	182	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to D \in P$
223		simplr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to e \in P$
224	179	ad3antrrr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to X \in P$
225		simpr	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to e \in (D I X)$
226	1 20 2 221 222 223 224 225	tgbtwncom	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land e \in (D I X)) \to e \in (X I D)$
227	226	adantrl	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to e \in (X I D)$
228	220 227	jca	$⊢ ((((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \land (e \in (A I B) \land e \in (D I X))) \to (A K (B) e \land e \in (X I D))$
229	228	ex	$⊢ (((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \land e \in P) \to ((e \in (A I B) \land e \in (D I X)) \to (A K (B) e \land e \in (X I D)))$
230	229	reximdva	$⊢ ((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \to (\exists e \in P (e \in (A I B) \land e \in (D I X)) \to \exists e \in P (A K (B) e \land e \in (X I D)))$
231	185 230	mpd	$⊢ ((φ \land D \in (B I C)) \land \neg X \in (B {Line}_{𝒢} (G) D)) \to \exists e \in P (A K (B) e \land e \in (X I D))$
232	177 231	pm2.61dan	$⊢ (φ \land D \in (B I C)) \to \exists e \in P (A K (B) e \land e \in (X I D))$
233	76	simp3d	$⊢ φ \to (C \in (B I D) \lor D \in (B I C))$
234	53 232 233	mpjaodan	$⊢ φ \to \exists e \in P (A K (B) e \land e \in (X I D))$

Metamath Proof Explorer

Theorem hlpasch

Proof