tglineelsb2

Description: If S lies on PQ , then PQ = PS . Theorem 6.16 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-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)$
Assertion	tglineelsb2	$⊢ φ \to P L Q = P L S$

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	4	adantr	$⊢ (φ \land x \in (P L Q)) \to G \in 𝒢_{Tarski}$
12	5	adantr	$⊢ (φ \land x \in (P L Q)) \to P \in B$
13	8	adantr	$⊢ (φ \land x \in (P L Q)) \to S \in B$
14	9	necomd	$⊢ φ \to P \neq S$
15	14	adantr	$⊢ (φ \land x \in (P L Q)) \to P \neq S$
16	6	adantr	$⊢ (φ \land x \in (P L Q)) \to Q \in B$
17	7	necomd	$⊢ φ \to Q \neq P$
18	17	adantr	$⊢ (φ \land x \in (P L Q)) \to Q \neq P$
19	10	adantr	$⊢ (φ \land x \in (P L Q)) \to S \in (P L Q)$
20	1 2 3 11 16 12 13 18 19	lncom	$⊢ (φ \land x \in (P L Q)) \to S \in (Q L P)$
21	1 2 3 11 12 13 16 15 20 18	lnrot1	$⊢ (φ \land x \in (P L Q)) \to Q \in (P L S)$
22	1 3 2 4 5 6 7	tglnssp	$⊢ φ \to P L Q \subseteq B$
23	22	sselda	$⊢ (φ \land x \in (P L Q)) \to x \in B$
24		simpr	$⊢ (φ \land x \in (P L Q)) \to x \in (P L Q)$
25	1 2 3 11 12 13 15 16 18 21 23 24	tglineeltr	$⊢ (φ \land x \in (P L Q)) \to x \in (P L S)$
26	4	adantr	$⊢ (φ \land x \in (P L S)) \to G \in 𝒢_{Tarski}$
27	5	adantr	$⊢ (φ \land x \in (P L S)) \to P \in B$
28	6	adantr	$⊢ (φ \land x \in (P L S)) \to Q \in B$
29	7	adantr	$⊢ (φ \land x \in (P L S)) \to P \neq Q$
30	8	adantr	$⊢ (φ \land x \in (P L S)) \to S \in B$
31	9	adantr	$⊢ (φ \land x \in (P L S)) \to S \neq P$
32	10	adantr	$⊢ (φ \land x \in (P L S)) \to S \in (P L Q)$
33	1 3 2 4 5 8 14	tglnssp	$⊢ φ \to P L S \subseteq B$
34	33	sselda	$⊢ (φ \land x \in (P L S)) \to x \in B$
35		simpr	$⊢ (φ \land x \in (P L S)) \to x \in (P L S)$
36	1 2 3 26 27 28 29 30 31 32 34 35	tglineeltr	$⊢ (φ \land x \in (P L S)) \to x \in (P L Q)$
37	25 36	impbida	$⊢ φ \to (x \in (P L Q) \leftrightarrow x \in (P L S))$
38	37	eqrdv	$⊢ φ \to P L Q = P L S$

Metamath Proof Explorer

Theorem tglineelsb2

Proof