tglineeltr

Description: Transitivity law for lines, one half of tglineelsb2 . (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	$⊢ B = {Base}_{G}$
	tglineelsb2.i	$⊢ I = Itv (G)$
	tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineelsb2.1	$⊢ φ \to P \in B$
	tglineelsb2.2	$⊢ φ \to Q \in B$
	tglineelsb2.4	$⊢ φ \to P \neq Q$
	tglineelsb2.3	$⊢ φ \to S \in B$
	tglineelsb2.5	$⊢ φ \to S \neq P$
	tglineelsb2.6	$⊢ φ \to S \in (P L Q)$
	tglineeltr.7	$⊢ φ \to R \in B$
	tglineeltr.8	$⊢ φ \to R \in (P L S)$
Assertion	tglineeltr	$⊢ φ \to R \in (P L Q)$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineelsb2.1	$⊢ φ \to P \in B$
6		tglineelsb2.2	$⊢ φ \to Q \in B$
7		tglineelsb2.4	$⊢ φ \to P \neq Q$
8		tglineelsb2.3	$⊢ φ \to S \in B$
9		tglineelsb2.5	$⊢ φ \to S \neq P$
10		tglineelsb2.6	$⊢ φ \to S \in (P L Q)$
11		tglineeltr.7	$⊢ φ \to R \in B$
12		tglineeltr.8	$⊢ φ \to R \in (P L S)$
13	4	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to G \in 𝒢_{Tarski}$
14	5	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to P \in B$
15	6	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to Q \in B$
16		simpllr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to R \in B$
17		eqid	$⊢ dist (G) = dist (G)$
18	8	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to S \in B$
19		simplr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to R \in (P I S)$
20		simpr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to S \in (P I Q)$
21	1 17 2 13 14 16 18 15 19 20	tgbtwnexch	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to R \in (P I Q)$
22	1 3 2 13 14 15 16 21	btwncolg1	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land S \in (P I Q)) \to (R \in (P L Q) \lor P = Q)$
23	4	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to G \in 𝒢_{Tarski}$
24	5	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to P \in B$
25	6	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to Q \in B$
26		simpllr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to R \in B$
27	8	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to S \in B$
28		simplr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to R \in (P I S)$
29	1 17 2 23 24 26 27 28	tgbtwncom	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to R \in (S I P)$
30		simpr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to P \in (S I Q)$
31	1 17 2 23 27 26 24 25 29 30	tgbtwnexch3	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to P \in (R I Q)$
32	1 3 2 23 24 25 26 31	btwncolg2	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land P \in (S I Q)) \to (R \in (P L Q) \lor P = Q)$
33	4	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to G \in 𝒢_{Tarski}$
34	5	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to P \in B$
35		simpllr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to R \in B$
36	6	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to Q \in B$
37	8	ad3antrrr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to S \in B$
38		simplr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to R \in (P I S)$
39		simpr	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to Q \in (P I S)$
40	1 2 33 34 35 36 37 38 39 3	tgbtwnconnln3	$⊢ (((φ \land R \in B) \land R \in (P I S)) \land Q \in (P I S)) \to (R \in (P L Q) \lor P = Q)$
41	1 3 2 4 5 6 7 8	tgellng	$⊢ φ \to (S \in (P L Q) \leftrightarrow (S \in (P I Q) \lor P \in (S I Q) \lor Q \in (P I S)))$
42	10 41	mpbid	$⊢ φ \to (S \in (P I Q) \lor P \in (S I Q) \lor Q \in (P I S))$
43	42	ad2antrr	$⊢ ((φ \land R \in B) \land R \in (P I S)) \to (S \in (P I Q) \lor P \in (S I Q) \lor Q \in (P I S))$
44	22 32 40 43	mpjao3dan	$⊢ ((φ \land R \in B) \land R \in (P I S)) \to (R \in (P L Q) \lor P = Q)$
45	44	an32s	$⊢ ((φ \land R \in (P I S)) \land R \in B) \to (R \in (P L Q) \lor P = Q)$
46	11 45	mpidan	$⊢ (φ \land R \in (P I S)) \to (R \in (P L Q) \lor P = Q)$
47	4	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to G \in 𝒢_{Tarski}$
48	5	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to P \in B$
49	6	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to Q \in B$
50		simpllr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to R \in B$
51	8	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to S \in B$
52	9	necomd	$⊢ φ \to P \neq S$
53	52	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to P \neq S$
54		simplr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to P \in (R I S)$
55		simpr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to S \in (P I Q)$
56	1 17 2 47 50 48 51 49 53 54 55	tgbtwnouttr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to P \in (R I Q)$
57	1 3 2 47 48 49 50 56	btwncolg2	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land S \in (P I Q)) \to (R \in (P L Q) \lor P = Q)$
58	4	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to G \in 𝒢_{Tarski}$
59	6	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to Q \in B$
60		simpllr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to R \in B$
61	5	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to P \in B$
62	8	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to S \in B$
63	9	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to S \neq P$
64		simpr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to P \in (S I Q)$
65		simplr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to P \in (R I S)$
66	1 17 2 58 60 61 62 65	tgbtwncom	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to P \in (S I R)$
67	1 2 58 62 61 59 60 3 63 64 66	tgbtwnconnln2	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to (P \in (Q L R) \lor Q = R)$
68	1 3 2 58 59 60 61 67	colrot2	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land P \in (S I Q)) \to (R \in (P L Q) \lor P = Q)$
69	4	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to G \in 𝒢_{Tarski}$
70	6	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to Q \in B$
71	5	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to P \in B$
72		simpllr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to R \in B$
73	8	ad3antrrr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to S \in B$
74		simpr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to Q \in (P I S)$
75		simplr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to P \in (R I S)$
76	1 17 2 69 70 71 72 73 74 75	tgbtwnintr	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to P \in (Q I R)$
77	1 3 2 69 70 71 72 76	btwncolg3	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to (R \in (Q L P) \lor Q = P)$
78	1 3 2 69 70 71 72 77	colcom	$⊢ (((φ \land R \in B) \land P \in (R I S)) \land Q \in (P I S)) \to (R \in (P L Q) \lor P = Q)$
79	42	ad2antrr	$⊢ ((φ \land R \in B) \land P \in (R I S)) \to (S \in (P I Q) \lor P \in (S I Q) \lor Q \in (P I S))$
80	57 68 78 79	mpjao3dan	$⊢ ((φ \land R \in B) \land P \in (R I S)) \to (R \in (P L Q) \lor P = Q)$
81	80	an32s	$⊢ ((φ \land P \in (R I S)) \land R \in B) \to (R \in (P L Q) \lor P = Q)$
82	11 81	mpidan	$⊢ (φ \land P \in (R I S)) \to (R \in (P L Q) \lor P = Q)$
83	4	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to G \in 𝒢_{Tarski}$
84	6	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to Q \in B$
85		simpllr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to R \in B$
86	5	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to P \in B$
87	8	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to S \in B$
88	52	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to P \neq S$
89		simpr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to S \in (P I Q)$
90		simplr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to S \in (P I R)$
91	1 2 83 86 87 84 85 3 88 89 90	tgbtwnconnln1	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to (P \in (Q L R) \lor Q = R)$
92	1 3 2 83 84 85 86 91	colrot2	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land S \in (P I Q)) \to (R \in (P L Q) \lor P = Q)$
93	4	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to G \in 𝒢_{Tarski}$
94	5	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to P \in B$
95	6	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to Q \in B$
96		simpllr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to R \in B$
97	8	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to S \in B$
98	9	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to S \neq P$
99		simplr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to S \in (P I R)$
100	1 17 2 93 94 97 96 99	tgbtwncom	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to S \in (R I P)$
101		simpr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to P \in (S I Q)$
102	1 17 2 93 96 97 94 95 98 100 101	tgbtwnouttr2	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to P \in (R I Q)$
103	1 3 2 93 94 95 96 102	btwncolg2	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land P \in (S I Q)) \to (R \in (P L Q) \lor P = Q)$
104	4	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to G \in 𝒢_{Tarski}$
105	5	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to P \in B$
106	6	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to Q \in B$
107		simpllr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to R \in B$
108	8	ad3antrrr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to S \in B$
109		simpr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to Q \in (P I S)$
110		simplr	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to S \in (P I R)$
111	1 17 2 104 105 106 108 107 109 110	tgbtwnexch	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to Q \in (P I R)$
112	1 3 2 104 105 106 107 111	btwncolg3	$⊢ (((φ \land R \in B) \land S \in (P I R)) \land Q \in (P I S)) \to (R \in (P L Q) \lor P = Q)$
113	42	ad2antrr	$⊢ ((φ \land R \in B) \land S \in (P I R)) \to (S \in (P I Q) \lor P \in (S I Q) \lor Q \in (P I S))$
114	92 103 112 113	mpjao3dan	$⊢ ((φ \land R \in B) \land S \in (P I R)) \to (R \in (P L Q) \lor P = Q)$
115	114	an32s	$⊢ ((φ \land S \in (P I R)) \land R \in B) \to (R \in (P L Q) \lor P = Q)$
116	11 115	mpidan	$⊢ (φ \land S \in (P I R)) \to (R \in (P L Q) \lor P = Q)$
117		id	$⊢ φ \to φ$
118	4	adantr	$⊢ (φ \land R \in B) \to G \in 𝒢_{Tarski}$
119	5	adantr	$⊢ (φ \land R \in B) \to P \in B$
120	8	adantr	$⊢ (φ \land R \in B) \to S \in B$
121	52	adantr	$⊢ (φ \land R \in B) \to P \neq S$
122		simpr	$⊢ (φ \land R \in B) \to R \in B$
123	1 3 2 118 119 120 121 122	tgellng	$⊢ (φ \land R \in B) \to (R \in (P L S) \leftrightarrow (R \in (P I S) \lor P \in (R I S) \lor S \in (P I R)))$
124	123	biimpa	$⊢ ((φ \land R \in B) \land R \in (P L S)) \to (R \in (P I S) \lor P \in (R I S) \lor S \in (P I R))$
125	117 11 12 124	syl21anc	$⊢ φ \to (R \in (P I S) \lor P \in (R I S) \lor S \in (P I R))$
126	46 82 116 125	mpjao3dan	$⊢ φ \to (R \in (P L Q) \lor P = Q)$
127	7	neneqd	$⊢ φ \to \neg P = Q$
128		pm5.61	$⊢ ((R \in (P L Q) \lor P = Q) \land \neg P = Q) \leftrightarrow (R \in (P L Q) \land \neg P = Q)$
129	128	simplbi	$⊢ ((R \in (P L Q) \lor P = Q) \land \neg P = Q) \to R \in (P L Q)$
130	126 127 129	syl2anc	$⊢ φ \to R \in (P L Q)$

Metamath Proof Explorer

Theorem tglineeltr

Proof