Metamath Proof Explorer

Theorem linethru

Description: If A is a line containing two distinct points P and Q , then A is the line through P and Q . Theorem 6.18 of Schwabhauser p. 45. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion linethru 
|- ( ( A e. LinesEE /\ ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) )

Proof

Step Hyp Ref Expression
1 ellines 
 |-  ( A e. LinesEE <-> E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) ( a =/= b /\ A = ( a Line b ) ) )
2 simpll1 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> n e. NN )
3 simpll2 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> a e. ( EE ` n ) )
4 simpll3 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> b e. ( EE ` n ) )
5 simplr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> a =/= b )
6 liness 
 |-  ( ( n e. NN /\ ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) ) -> ( a Line b ) C_ ( EE ` n ) )
7 2 3 4 5 6 syl13anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> ( a Line b ) C_ ( EE ` n ) )
8 simprll 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> P e. ( a Line b ) )
9 7 8 sseldd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> P e. ( EE ` n ) )
10 simprlr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> Q e. ( a Line b ) )
11 7 10 sseldd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> Q e. ( EE ` n ) )
12 simplll 
 |-  ( ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) -> P e. ( a Line b ) )
13 12 adantl 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> P e. ( a Line b ) )
14 simpll1 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> n e. NN )
15 simpll2 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> a e. ( EE ` n ) )
16 simpll3 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> b e. ( EE ` n ) )
17 simplr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> a =/= b )
18 simprrl 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> P e. ( EE ` n ) )
19 simprlr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> P =/= a )
20 19 necomd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> a =/= P )
21 lineelsb2 
 |-  ( ( n e. NN /\ ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ ( P e. ( EE ` n ) /\ a =/= P ) ) -> ( P e. ( a Line b ) -> ( a Line b ) = ( a Line P ) ) )
22 14 15 16 17 18 20 21 syl132anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( P e. ( a Line b ) -> ( a Line b ) = ( a Line P ) ) )
23 13 22 mpd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( a Line P ) )
24 linecom 
 |-  ( ( n e. NN /\ ( a e. ( EE ` n ) /\ P e. ( EE ` n ) /\ a =/= P ) ) -> ( a Line P ) = ( P Line a ) )
25 14 15 18 20 24 syl13anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line P ) = ( P Line a ) )
26 23 25 eqtrd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line a ) )
27 neeq2 
 |-  ( Q = a -> ( P =/= Q <-> P =/= a ) )
28 27 anbi2d 
 |-  ( Q = a -> ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) <-> ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) ) )
29 28 anbi1d 
 |-  ( Q = a -> ( ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) <-> ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) )
30 29 anbi2d 
 |-  ( Q = a -> ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) <-> ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) ) )
31 oveq2 
 |-  ( Q = a -> ( P Line Q ) = ( P Line a ) )
32 31 eqeq2d 
 |-  ( Q = a -> ( ( a Line b ) = ( P Line Q ) <-> ( a Line b ) = ( P Line a ) ) )
33 30 32 imbi12d 
 |-  ( Q = a -> ( ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line Q ) ) <-> ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= a ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line a ) ) ) )
34 26 33 mpbiri 
 |-  ( Q = a -> ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line Q ) ) )
35 simp1 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) )
36 simp2l 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) )
37 35 36 10 syl2anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> Q e. ( a Line b ) )
38 simp1l1 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> n e. NN )
39 simp1l2 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> a e. ( EE ` n ) )
40 simp1l3 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> b e. ( EE ` n ) )
41 simp1r 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> a =/= b )
42 simp2rr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> Q e. ( EE ` n ) )
43 simp3 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> Q =/= a )
44 43 necomd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> a =/= Q )
45 lineelsb2 
 |-  ( ( n e. NN /\ ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ ( Q e. ( EE ` n ) /\ a =/= Q ) ) -> ( Q e. ( a Line b ) -> ( a Line b ) = ( a Line Q ) ) )
46 38 39 40 41 42 44 45 syl132anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( Q e. ( a Line b ) -> ( a Line b ) = ( a Line Q ) ) )
47 37 46 mpd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( a Line b ) = ( a Line Q ) )
48 linecom 
 |-  ( ( n e. NN /\ ( a e. ( EE ` n ) /\ Q e. ( EE ` n ) /\ a =/= Q ) ) -> ( a Line Q ) = ( Q Line a ) )
49 38 39 42 44 48 syl13anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( a Line Q ) = ( Q Line a ) )
50 47 49 eqtrd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( a Line b ) = ( Q Line a ) )
51 36 simplld 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> P e. ( a Line b ) )
52 51 50 eleqtrd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> P e. ( Q Line a ) )
53 simp2rl 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> P e. ( EE ` n ) )
54 simp2lr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> P =/= Q )
55 54 necomd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> Q =/= P )
56 lineelsb2 
 |-  ( ( n e. NN /\ ( Q e. ( EE ` n ) /\ a e. ( EE ` n ) /\ Q =/= a ) /\ ( P e. ( EE ` n ) /\ Q =/= P ) ) -> ( P e. ( Q Line a ) -> ( Q Line a ) = ( Q Line P ) ) )
57 38 42 39 43 53 55 56 syl132anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( P e. ( Q Line a ) -> ( Q Line a ) = ( Q Line P ) ) )
58 52 57 mpd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( Q Line a ) = ( Q Line P ) )
59 linecom 
 |-  ( ( n e. NN /\ ( Q e. ( EE ` n ) /\ P e. ( EE ` n ) /\ Q =/= P ) ) -> ( Q Line P ) = ( P Line Q ) )
60 38 42 53 55 59 syl13anc 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( Q Line P ) = ( P Line Q ) )
61 50 58 60 3eqtrd 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) /\ Q =/= a ) -> ( a Line b ) = ( P Line Q ) )
62 61 3expa 
 |-  ( ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) /\ Q =/= a ) -> ( a Line b ) = ( P Line Q ) )
63 62 expcom 
 |-  ( Q =/= a -> ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line Q ) ) )
64 34 63 pm2.61ine 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) /\ ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) ) ) -> ( a Line b ) = ( P Line Q ) )
65 64 expr 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> ( ( P e. ( EE ` n ) /\ Q e. ( EE ` n ) ) -> ( a Line b ) = ( P Line Q ) ) )
66 9 11 65 mp2and 
 |-  ( ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) /\ ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) -> ( a Line b ) = ( P Line Q ) )
67 66 ex 
 |-  ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) -> ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) -> ( a Line b ) = ( P Line Q ) ) )
68 eleq2 
 |-  ( A = ( a Line b ) -> ( P e. A <-> P e. ( a Line b ) ) )
69 eleq2 
 |-  ( A = ( a Line b ) -> ( Q e. A <-> Q e. ( a Line b ) ) )
70 68 69 anbi12d 
 |-  ( A = ( a Line b ) -> ( ( P e. A /\ Q e. A ) <-> ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) ) )
71 70 anbi1d 
 |-  ( A = ( a Line b ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) <-> ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) ) )
72 eqeq1 
 |-  ( A = ( a Line b ) -> ( A = ( P Line Q ) <-> ( a Line b ) = ( P Line Q ) ) )
73 71 72 imbi12d 
 |-  ( A = ( a Line b ) -> ( ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) <-> ( ( ( P e. ( a Line b ) /\ Q e. ( a Line b ) ) /\ P =/= Q ) -> ( a Line b ) = ( P Line Q ) ) ) )
74 67 73 syl5ibrcom 
 |-  ( ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) /\ a =/= b ) -> ( A = ( a Line b ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) ) )
75 74 expimpd 
 |-  ( ( n e. NN /\ a e. ( EE ` n ) /\ b e. ( EE ` n ) ) -> ( ( a =/= b /\ A = ( a Line b ) ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) ) )
76 75 3expa 
 |-  ( ( ( n e. NN /\ a e. ( EE ` n ) ) /\ b e. ( EE ` n ) ) -> ( ( a =/= b /\ A = ( a Line b ) ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) ) )
77 76 rexlimdva 
 |-  ( ( n e. NN /\ a e. ( EE ` n ) ) -> ( E. b e. ( EE ` n ) ( a =/= b /\ A = ( a Line b ) ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) ) )
78 77 rexlimivv 
 |-  ( E. n e. NN E. a e. ( EE ` n ) E. b e. ( EE ` n ) ( a =/= b /\ A = ( a Line b ) ) -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) )
79 1 78 sylbi 
 |-  ( A e. LinesEE -> ( ( ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) ) )
80 79 3impib 
 |-  ( ( A e. LinesEE /\ ( P e. A /\ Q e. A ) /\ P =/= Q ) -> A = ( P Line Q ) )