Metamath Proof Explorer

Theorem linecom

Description: Commutativity law for lines. Part of theorem 6.17 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	linecom	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = Q Line P$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land x \in 𝔼 (N)) \to N \in ℕ$
2		simp3	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
3		simp21	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land x \in 𝔼 (N)) \to P \in 𝔼 (N)$
4		simp22	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land x \in 𝔼 (N)) \to Q \in 𝔼 (N)$
5		colinearperm1	$⊢ (N \in ℕ \land (x \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \in 𝔼 (N))) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨Q, P⟩)$
6	1 2 3 4 5	syl13anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨Q, P⟩)$
7	6	3expa	$⊢ ((N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \land x \in 𝔼 (N)) \to (x Colinear ⟨P, Q⟩ \leftrightarrow x Colinear ⟨Q, P⟩)$
8	7	rabbidva	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\} = \{x \in 𝔼 (N) \| x Colinear ⟨Q, P⟩\}$
9		fvline2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = \{x \in 𝔼 (N) \| x Colinear ⟨P, Q⟩\}$
10		necom	$⊢ P \neq Q \leftrightarrow Q \neq P$
11	10	3anbi3i	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \leftrightarrow (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land Q \neq P)$
12		3ancoma	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land Q \neq P) \leftrightarrow (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)$
13	11 12	bitri	$⊢ (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q) \leftrightarrow (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)$
14		fvline2	$⊢ (N \in ℕ \land (Q \in 𝔼 (N) \land P \in 𝔼 (N) \land Q \neq P)) \to Q Line P = \{x \in 𝔼 (N) \| x Colinear ⟨Q, P⟩\}$
15	13 14	sylan2b	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to Q Line P = \{x \in 𝔼 (N) \| x Colinear ⟨Q, P⟩\}$
16	8 9 15	3eqtr4d	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land Q \in 𝔼 (N) \land P \neq Q)) \to P Line Q = Q Line P$