lnext

Description: Extend a line with a missing point. Theorem 4.14 of Schwabhauser p. 37. (Contributed by Thierry Arnoux, 27-Apr-2019)

	Ref	Expression
Hypotheses	tglngval.p	$⊢ P = {Base}_{G}$
	tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
	tglngval.i	$⊢ I = Itv (G)$
	tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglngval.x	$⊢ φ \to X \in P$
	tglngval.y	$⊢ φ \to Y \in P$
	tgcolg.z	$⊢ φ \to Z \in P$
	lnxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
	lnxfr.a	$⊢ φ \to A \in P$
	lnxfr.b	$⊢ φ \to B \in P$
	lnxfr.d	$⊢ \underset{˙}{-} = dist (G)$
	lnext.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
	lnext.2	$⊢ φ \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
Assertion	lnext	$⊢ φ \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$

Proof

Step	Hyp	Ref	Expression
1		tglngval.p	$⊢ P = {Base}_{G}$
2		tglngval.l	$⊢ L = {Line}_{𝒢} (G)$
3		tglngval.i	$⊢ I = Itv (G)$
4		tglngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglngval.x	$⊢ φ \to X \in P$
6		tglngval.y	$⊢ φ \to Y \in P$
7		tgcolg.z	$⊢ φ \to Z \in P$
8		lnxfr.r	$⊢ \underset{˙}{\sim} = \sim_{𝒢} (G)$
9		lnxfr.a	$⊢ φ \to A \in P$
10		lnxfr.b	$⊢ φ \to B \in P$
11		lnxfr.d	$⊢ \underset{˙}{-} = dist (G)$
12		lnext.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
13		lnext.2	$⊢ φ \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
14	1 11 3 4 9 10 6 7	axtgsegcon	$⊢ φ \to \exists c \in P (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)$
15	14	adantr	$⊢ (φ \land Y \in (X I Z)) \to \exists c \in P (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)$
16	4	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to G \in 𝒢_{Tarski}$
17	5	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to X \in P$
18	6	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to Y \in P$
19	7	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to Z \in P$
20	9	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to A \in P$
21	10	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to B \in P$
22		simplr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to c \in P$
23	13	ad3antrrr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
24		simprr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to B \underset{˙}{-} c = Y \underset{˙}{-} Z$
25	24	eqcomd	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to Y \underset{˙}{-} Z = B \underset{˙}{-} c$
26		simpllr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to Y \in (X I Z)$
27		simprl	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to B \in (A I c)$
28	1 11 3 16 17 18 19 20 21 22 26 27 23 25	tgcgrextend	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to X \underset{˙}{-} Z = A \underset{˙}{-} c$
29	1 11 3 16 17 19 20 22 28	tgcgrcomlr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to Z \underset{˙}{-} X = c \underset{˙}{-} A$
30	1 11 8 16 17 18 19 20 21 22 23 25 29	trgcgr	$⊢ (((φ \land Y \in (X I Z)) \land c \in P) \land (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
31	30	ex	$⊢ ((φ \land Y \in (X I Z)) \land c \in P) \to ((B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
32	31	reximdva	$⊢ (φ \land Y \in (X I Z)) \to (\exists c \in P (B \in (A I c) \land B \underset{˙}{-} c = Y \underset{˙}{-} Z) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
33	15 32	mpd	$⊢ (φ \land Y \in (X I Z)) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
34	1 11 3 4 10 9 5 7	axtgsegcon	$⊢ φ \to \exists c \in P (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)$
35	34	adantr	$⊢ (φ \land X \in (Y I Z)) \to \exists c \in P (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)$
36	4	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to G \in 𝒢_{Tarski}$
37	5	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to X \in P$
38	6	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to Y \in P$
39	7	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to Z \in P$
40	9	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to A \in P$
41	10	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to B \in P$
42		simplr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to c \in P$
43	13	ad3antrrr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
44		simpllr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to X \in (Y I Z)$
45		simprl	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to A \in (B I c)$
46	1 11 3 36 37 38 40 41 43	tgcgrcomlr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to Y \underset{˙}{-} X = B \underset{˙}{-} A$
47		simprr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to A \underset{˙}{-} c = X \underset{˙}{-} Z$
48	47	eqcomd	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to X \underset{˙}{-} Z = A \underset{˙}{-} c$
49	1 11 3 36 38 37 39 41 40 42 44 45 46 48	tgcgrextend	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to Y \underset{˙}{-} Z = B \underset{˙}{-} c$
50	1 11 3 36 37 39 40 42 48	tgcgrcomlr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to Z \underset{˙}{-} X = c \underset{˙}{-} A$
51	1 11 8 36 37 38 39 40 41 42 43 49 50	trgcgr	$⊢ (((φ \land X \in (Y I Z)) \land c \in P) \land (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
52	51	ex	$⊢ ((φ \land X \in (Y I Z)) \land c \in P) \to ((A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
53	52	reximdva	$⊢ (φ \land X \in (Y I Z)) \to (\exists c \in P (A \in (B I c) \land A \underset{˙}{-} c = X \underset{˙}{-} Z) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
54	35 53	mpd	$⊢ (φ \land X \in (Y I Z)) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
55	4	adantr	$⊢ (φ \land Z \in (X I Y)) \to G \in 𝒢_{Tarski}$
56	5	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \in P$
57	7	adantr	$⊢ (φ \land Z \in (X I Y)) \to Z \in P$
58	6	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \in P$
59	9	adantr	$⊢ (φ \land Z \in (X I Y)) \to A \in P$
60	10	adantr	$⊢ (φ \land Z \in (X I Y)) \to B \in P$
61		simpr	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X I Y)$
62	13	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
63	1 11 3 8 55 56 57 58 59 60 61 62	tgcgrxfr	$⊢ (φ \land Z \in (X I Y)) \to \exists c \in P (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)$
64	4	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to G \in 𝒢_{Tarski}$
65	5	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to X \in P$
66	7	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to Z \in P$
67	6	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to Y \in P$
68	9	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to A \in P$
69		simplr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to c \in P$
70	10	ad3antrrr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to B \in P$
71		simprr	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩$
72	1 11 3 8 64 65 66 67 68 69 70 71	cgr3swap23	$⊢ (((φ \land Z \in (X I Y)) \land c \in P) \land (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
73	72	ex	$⊢ ((φ \land Z \in (X I Y)) \land c \in P) \to ((c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
74	73	reximdva	$⊢ (φ \land Z \in (X I Y)) \to (\exists c \in P (c \in (A I B) \land ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A c B ”⟩) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩)$
75	63 74	mpd	$⊢ (φ \land Z \in (X I Y)) \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$
76	1 2 3 4 5 7 6	tgcolg	$⊢ φ \to ((Y \in (X L Z) \lor X = Z) \leftrightarrow (Y \in (X I Z) \lor X \in (Y I Z) \lor Z \in (X I Y)))$
77	12 76	mpbid	$⊢ φ \to (Y \in (X I Z) \lor X \in (Y I Z) \lor Z \in (X I Y))$
78	33 54 75 77	mpjao3dan	$⊢ φ \to \exists c \in P ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B c ”⟩$

Metamath Proof Explorer

Theorem lnext

Proof