Metamath Proof Explorer

Theorem fvline

Description: Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvline 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x | x Colinear <. A , B >. } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear
2 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
3 2 eleq2d 
 |-  ( n = N -> ( A e. ( EE ` n ) <-> A e. ( EE ` N ) ) )
4 2 eleq2d 
 |-  ( n = N -> ( B e. ( EE ` n ) <-> B e. ( EE ` N ) ) )
5 3 4 3anbi12d 
 |-  ( n = N -> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) )
6 5 anbi1d 
 |-  ( n = N -> ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) <-> ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
7 6 rspcev 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) -> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) )
8 1 7 mpanr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) )
9 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> A e. ( EE ` N ) )
10 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> B e. ( EE ` N ) )
11 colinearex 
 |-  Colinear e. _V
12 11 cnvex 
 |-  `' Colinear e. _V
13 ecexg 
 |-  ( `' Colinear e. _V -> [ <. A , B >. ] `' Colinear e. _V )
14 12 13 ax-mp 
 |-  [ <. A , B >. ] `' Colinear e. _V
15 eleq1 
 |-  ( a = A -> ( a e. ( EE ` n ) <-> A e. ( EE ` n ) ) )
16 neeq1 
 |-  ( a = A -> ( a =/= b <-> A =/= b ) )
17 15 16 3anbi13d 
 |-  ( a = A -> ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) <-> ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) ) )
18 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
19 18 eceq1d 
 |-  ( a = A -> [ <. a , b >. ] `' Colinear = [ <. A , b >. ] `' Colinear )
20 19 eqeq2d 
 |-  ( a = A -> ( l = [ <. a , b >. ] `' Colinear <-> l = [ <. A , b >. ] `' Colinear ) )
21 17 20 anbi12d 
 |-  ( a = A -> ( ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> ( ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) /\ l = [ <. A , b >. ] `' Colinear ) ) )
22 21 rexbidv 
 |-  ( a = A -> ( E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) /\ l = [ <. A , b >. ] `' Colinear ) ) )
23 eleq1 
 |-  ( b = B -> ( b e. ( EE ` n ) <-> B e. ( EE ` n ) ) )
24 neeq2 
 |-  ( b = B -> ( A =/= b <-> A =/= B ) )
25 23 24 3anbi23d 
 |-  ( b = B -> ( ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) <-> ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) ) )
26 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
27 26 eceq1d 
 |-  ( b = B -> [ <. A , b >. ] `' Colinear = [ <. A , B >. ] `' Colinear )
28 27 eqeq2d 
 |-  ( b = B -> ( l = [ <. A , b >. ] `' Colinear <-> l = [ <. A , B >. ] `' Colinear ) )
29 25 28 anbi12d 
 |-  ( b = B -> ( ( ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) /\ l = [ <. A , b >. ] `' Colinear ) <-> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ l = [ <. A , B >. ] `' Colinear ) ) )
30 29 rexbidv 
 |-  ( b = B -> ( E. n e. NN ( ( A e. ( EE ` n ) /\ b e. ( EE ` n ) /\ A =/= b ) /\ l = [ <. A , b >. ] `' Colinear ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ l = [ <. A , B >. ] `' Colinear ) ) )
31 eqeq1 
 |-  ( l = [ <. A , B >. ] `' Colinear -> ( l = [ <. A , B >. ] `' Colinear <-> [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) )
32 31 anbi2d 
 |-  ( l = [ <. A , B >. ] `' Colinear -> ( ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ l = [ <. A , B >. ] `' Colinear ) <-> ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
33 32 rexbidv 
 |-  ( l = [ <. A , B >. ] `' Colinear -> ( E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ l = [ <. A , B >. ] `' Colinear ) <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
34 22 30 33 eloprabg 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ [ <. A , B >. ] `' Colinear e. _V ) -> ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
35 14 34 mp3an3 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
36 9 10 35 syl2anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } <-> E. n e. NN ( ( A e. ( EE ` n ) /\ B e. ( EE ` n ) /\ A =/= B ) /\ [ <. A , B >. ] `' Colinear = [ <. A , B >. ] `' Colinear ) ) )
37 8 36 mpbird 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } )
38 df-ov 
 |-  ( A Line B ) = ( Line ` <. A , B >. )
39 df-br 
 |-  ( <. A , B >. Line [ <. A , B >. ] `' Colinear <-> <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. Line )
40 df-line2 
 |-  Line = { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) }
41 40 eleq2i 
 |-  ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. Line <-> <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } )
42 39 41 bitri 
 |-  ( <. A , B >. Line [ <. A , B >. ] `' Colinear <-> <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } )
43 funline 
 |-  Fun Line
44 funbrfv 
 |-  ( Fun Line -> ( <. A , B >. Line [ <. A , B >. ] `' Colinear -> ( Line ` <. A , B >. ) = [ <. A , B >. ] `' Colinear ) )
45 43 44 ax-mp 
 |-  ( <. A , B >. Line [ <. A , B >. ] `' Colinear -> ( Line ` <. A , B >. ) = [ <. A , B >. ] `' Colinear )
46 42 45 sylbir 
 |-  ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } -> ( Line ` <. A , B >. ) = [ <. A , B >. ] `' Colinear )
47 38 46 eqtrid 
 |-  ( <. <. A , B >. , [ <. A , B >. ] `' Colinear >. e. { <. <. a , b >. , l >. | E. n e. NN ( ( a e. ( EE ` n ) /\ b e. ( EE ` n ) /\ a =/= b ) /\ l = [ <. a , b >. ] `' Colinear ) } -> ( A Line B ) = [ <. A , B >. ] `' Colinear )
48 37 47 syl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = [ <. A , B >. ] `' Colinear )
49 opex 
 |-  <. A , B >. e. _V
50 dfec2 
 |-  ( <. A , B >. e. _V -> [ <. A , B >. ] `' Colinear = { x | <. A , B >. `' Colinear x } )
51 49 50 ax-mp 
 |-  [ <. A , B >. ] `' Colinear = { x | <. A , B >. `' Colinear x }
52 vex 
 |-  x e. _V
53 49 52 brcnv 
 |-  ( <. A , B >. `' Colinear x <-> x Colinear <. A , B >. )
54 53 abbii 
 |-  { x | <. A , B >. `' Colinear x } = { x | x Colinear <. A , B >. }
55 51 54 eqtri 
 |-  [ <. A , B >. ] `' Colinear = { x | x Colinear <. A , B >. }
56 48 55 eqtrdi 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ A =/= B ) ) -> ( A Line B ) = { x | x Colinear <. A , B >. } )