lnxfr

Description: Transfer law for colinearity. Theorem 4.13 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.c	$⊢ φ \to C \in P$
	lnxfr.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
	lnxfr.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
Assertion	lnxfr	$⊢ φ \to (B \in (A L C) \lor A = 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.c	$⊢ φ \to C \in P$
12		lnxfr.1	$⊢ φ \to (Y \in (X L Z) \lor X = Z)$
13		lnxfr.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
14	4	adantr	$⊢ (φ \land Y \in (X I Z)) \to G \in 𝒢_{Tarski}$
15	9	adantr	$⊢ (φ \land Y \in (X I Z)) \to A \in P$
16	11	adantr	$⊢ (φ \land Y \in (X I Z)) \to C \in P$
17	10	adantr	$⊢ (φ \land Y \in (X I Z)) \to B \in P$
18		eqid	$⊢ dist (G) = dist (G)$
19	5	adantr	$⊢ (φ \land Y \in (X I Z)) \to X \in P$
20	6	adantr	$⊢ (φ \land Y \in (X I Z)) \to Y \in P$
21	7	adantr	$⊢ (φ \land Y \in (X I Z)) \to Z \in P$
22	13	adantr	$⊢ (φ \land Y \in (X I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
23		simpr	$⊢ (φ \land Y \in (X I Z)) \to Y \in (X I Z)$
24	1 18 3 8 14 19 20 21 15 17 16 22 23	tgbtwnxfr	$⊢ (φ \land Y \in (X I Z)) \to B \in (A I C)$
25	1 2 3 14 15 16 17 24	btwncolg1	$⊢ (φ \land Y \in (X I Z)) \to (B \in (A L C) \lor A = C)$
26	4	adantr	$⊢ (φ \land X \in (Y I Z)) \to G \in 𝒢_{Tarski}$
27	9	adantr	$⊢ (φ \land X \in (Y I Z)) \to A \in P$
28	11	adantr	$⊢ (φ \land X \in (Y I Z)) \to C \in P$
29	10	adantr	$⊢ (φ \land X \in (Y I Z)) \to B \in P$
30	6	adantr	$⊢ (φ \land X \in (Y I Z)) \to Y \in P$
31	5	adantr	$⊢ (φ \land X \in (Y I Z)) \to X \in P$
32	7	adantr	$⊢ (φ \land X \in (Y I Z)) \to Z \in P$
33	13	adantr	$⊢ (φ \land X \in (Y I Z)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
34	1 18 3 8 26 31 30 32 27 29 28 33	cgr3swap12	$⊢ (φ \land X \in (Y I Z)) \to ⟨“ Y X Z ”⟩ \underset{˙}{\sim} ⟨“ B A C ”⟩$
35		simpr	$⊢ (φ \land X \in (Y I Z)) \to X \in (Y I Z)$
36	1 18 3 8 26 30 31 32 29 27 28 34 35	tgbtwnxfr	$⊢ (φ \land X \in (Y I Z)) \to A \in (B I C)$
37	1 2 3 26 27 28 29 36	btwncolg2	$⊢ (φ \land X \in (Y I Z)) \to (B \in (A L C) \lor A = C)$
38	4	adantr	$⊢ (φ \land Z \in (X I Y)) \to G \in 𝒢_{Tarski}$
39	9	adantr	$⊢ (φ \land Z \in (X I Y)) \to A \in P$
40	11	adantr	$⊢ (φ \land Z \in (X I Y)) \to C \in P$
41	10	adantr	$⊢ (φ \land Z \in (X I Y)) \to B \in P$
42	5	adantr	$⊢ (φ \land Z \in (X I Y)) \to X \in P$
43	7	adantr	$⊢ (φ \land Z \in (X I Y)) \to Z \in P$
44	6	adantr	$⊢ (φ \land Z \in (X I Y)) \to Y \in P$
45	13	adantr	$⊢ (φ \land Z \in (X I Y)) \to ⟨“ X Y Z ”⟩ \underset{˙}{\sim} ⟨“ A B C ”⟩$
46	1 18 3 8 38 42 44 43 39 41 40 45	cgr3swap23	$⊢ (φ \land Z \in (X I Y)) \to ⟨“ X Z Y ”⟩ \underset{˙}{\sim} ⟨“ A C B ”⟩$
47		simpr	$⊢ (φ \land Z \in (X I Y)) \to Z \in (X I Y)$
48	1 18 3 8 38 42 43 44 39 40 41 46 47	tgbtwnxfr	$⊢ (φ \land Z \in (X I Y)) \to C \in (A I B)$
49	1 2 3 38 39 40 41 48	btwncolg3	$⊢ (φ \land Z \in (X I Y)) \to (B \in (A L C) \lor A = C)$
50	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)))$
51	12 50	mpbid	$⊢ φ \to (Y \in (X I Z) \lor X \in (Y I Z) \lor Z \in (X I Y))$
52	25 37 49 51	mpjao3dan	$⊢ φ \to (B \in (A L C) \lor A = C)$

Metamath Proof Explorer

Theorem lnxfr

Proof