tglinecom

Description: Commutativity law for lines. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-May-2019)

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

Metamath Proof Explorer