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 e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = ( Q Line P ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ x e. ( EE ` N ) ) -> N e. NN )
2 simp3 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
3 simp21 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ x e. ( EE ` N ) ) -> P e. ( EE ` N ) )
4 simp22 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ x e. ( EE ` N ) ) -> Q e. ( EE ` N ) )
5 colinearperm1 
 |-  ( ( N e. NN /\ ( x e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q e. ( EE ` N ) ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. Q , P >. ) )
6 1 2 3 4 5 syl13anc 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) /\ x e. ( EE ` N ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. Q , P >. ) )
7 6 3expa 
 |-  ( ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) /\ x e. ( EE ` N ) ) -> ( x Colinear <. P , Q >. <-> x Colinear <. Q , P >. ) )
8 7 rabbidva 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> { x e. ( EE ` N ) | x Colinear <. P , Q >. } = { x e. ( EE ` N ) | x Colinear <. Q , P >. } )
9 fvline2 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = { x e. ( EE ` N ) | x Colinear <. P , Q >. } )
10 necom 
 |-  ( P =/= Q <-> Q =/= P )
11 10 3anbi3i 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) <-> ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ Q =/= P ) )
12 3ancoma 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ Q =/= P ) <-> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) )
13 11 12 bitri 
 |-  ( ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) <-> ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) )
14 fvline2 
 |-  ( ( N e. NN /\ ( Q e. ( EE ` N ) /\ P e. ( EE ` N ) /\ Q =/= P ) ) -> ( Q Line P ) = { x e. ( EE ` N ) | x Colinear <. Q , P >. } )
15 13 14 sylan2b 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( Q Line P ) = { x e. ( EE ` N ) | x Colinear <. Q , P >. } )
16 8 9 15 3eqtr4d 
 |-  ( ( N e. NN /\ ( P e. ( EE ` N ) /\ Q e. ( EE ` N ) /\ P =/= Q ) ) -> ( P Line Q ) = ( Q Line P ) )