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	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) = ( 𝑄 Line 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ )
2		simp3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
3		simp21	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
4		simp22	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
5		colinearperm1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ ↔ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ ) )
6	1 2 3 4 5	syl13anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ ↔ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ ) )
7	6	3expa	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ ↔ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ ) )
8	7	rabbidva	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ } = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ } )
9		fvline2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑃 , 𝑄 ⟩ } )
10		necom	⊢ ( 𝑃 ≠ 𝑄 ↔ 𝑄 ≠ 𝑃 )
11	10	3anbi3i	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
12		3ancoma	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) ↔ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
13	11 12	bitri	⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ↔ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) )
14		fvline2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ≠ 𝑃 ) ) → ( 𝑄 Line 𝑃 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ } )
15	13 14	sylan2b	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑄 Line 𝑃 ) = { 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑥 Colinear ⟨ 𝑄 , 𝑃 ⟩ } )
16	8 9 15	3eqtr4d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ≠ 𝑄 ) ) → ( 𝑃 Line 𝑄 ) = ( 𝑄 Line 𝑃 ) )