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 ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Line Q = Q Line P

Proof

Step Hyp Ref Expression
1 simp1 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → N ∈ ℕ
2 simp3 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → x ∈ 𝔼 ⁡ N
3 simp21 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → P ∈ 𝔼 ⁡ N
4 simp22 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → Q ∈ 𝔼 ⁡ N
5 colinearperm1 ⊢ N ∈ ℕ ∧ x ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N → x Colinear P Q ↔ x Colinear Q P
6 1 2 3 4 5 syl13anc ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → x Colinear P Q ↔ x Colinear Q P
7 6 3expa ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ∧ x ∈ 𝔼 ⁡ N → x Colinear P Q ↔ x Colinear Q P
8 7 rabbidva ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → x ∈ 𝔼 ⁡ N | x Colinear P Q = x ∈ 𝔼 ⁡ N | x Colinear Q P
9 fvline2 ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Line Q = x ∈ 𝔼 ⁡ N | x Colinear P Q
10 necom ⊢ P ≠ Q ↔ Q ≠ P
11 10 3anbi3i ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ↔ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ Q ≠ P
12 3ancoma ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ Q ≠ P ↔ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P
13 11 12 bitri ⊢ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q ↔ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P
14 fvline2 ⊢ N ∈ ℕ ∧ Q ∈ 𝔼 ⁡ N ∧ P ∈ 𝔼 ⁡ N ∧ Q ≠ P → Q Line P = x ∈ 𝔼 ⁡ N | x Colinear Q P
15 13 14 sylan2b ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → Q Line P = x ∈ 𝔼 ⁡ N | x Colinear Q P
16 8 9 15 3eqtr4d ⊢ N ∈ ℕ ∧ P ∈ 𝔼 ⁡ N ∧ Q ∈ 𝔼 ⁡ N ∧ P ≠ Q → P Line Q = Q Line P