Metamath Proof Explorer

Theorem fvtransport

Description: Calculate the value of the TransportTo function. This function takes four points, A through D , where C and D are distinct. It then returns the point that extends C D by the length of A B . (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvtransport 
|- ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( <. A , B >. TransportTo <. C , D >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( <. A , B >. TransportTo <. C , D >. ) = ( TransportTo ` <. <. A , B >. , <. C , D >. >. )
2 opelxpi 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
3 2 3ad2ant1 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
4 opelxpi 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
5 4 3ad2ant2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) )
6 simp3 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> C =/= D )
7 op1stg 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( 1st ` <. C , D >. ) = C )
8 7 3ad2ant2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( 1st ` <. C , D >. ) = C )
9 op2ndg 
 |-  ( ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) -> ( 2nd ` <. C , D >. ) = D )
10 9 3ad2ant2 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( 2nd ` <. C , D >. ) = D )
11 6 8 10 3netr4d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) )
12 3 5 11 3jca 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) )
13 8 opeq1d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> <. ( 1st ` <. C , D >. ) , r >. = <. C , r >. )
14 10 13 breq12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. <-> D Btwn <. C , r >. ) )
15 10 opeq1d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> <. ( 2nd ` <. C , D >. ) , r >. = <. D , r >. )
16 15 breq1d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. <-> <. D , r >. Cgr <. A , B >. ) )
17 14 16 anbi12d 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) <-> ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )
18 17 riotabidv 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )
19 18 eqcomd 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) )
20 12 19 jca 
 |-  ( ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) -> ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
21 fveq2 
 |-  ( n = N -> ( EE ` n ) = ( EE ` N ) )
22 21 sqxpeqd 
 |-  ( n = N -> ( ( EE ` n ) X. ( EE ` n ) ) = ( ( EE ` N ) X. ( EE ` N ) ) )
23 22 eleq2d 
 |-  ( n = N -> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
24 22 eleq2d 
 |-  ( n = N -> ( <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) ) )
25 23 24 3anbi12d 
 |-  ( n = N -> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) <-> ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) ) )
26 21 riotaeqdv 
 |-  ( n = N -> ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) )
27 26 eqeq2d 
 |-  ( n = N -> ( ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) <-> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
28 25 27 anbi12d 
 |-  ( n = N -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) <-> ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
29 28 rspcev 
 |-  ( ( N e. NN /\ ( ( <. A , B >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ <. C , D >. e. ( ( EE ` N ) X. ( EE ` N ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` N ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
30 20 29 sylan2 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
31 df-br 
 |-  ( <. <. A , B >. , <. C , D >. >. TransportTo ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) <-> <. <. <. A , B >. , <. C , D >. >. , ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) >. e. TransportTo )
32 df-transport 
 |-  TransportTo = { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) }
33 32 eleq2i 
 |-  ( <. <. <. A , B >. , <. C , D >. >. , ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) >. e. TransportTo <-> <. <. <. A , B >. , <. C , D >. >. , ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) >. e. { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) } )
34 opex 
 |-  <. A , B >. e. _V
35 opex 
 |-  <. C , D >. e. _V
36 riotaex 
 |-  ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) e. _V
37 eleq1 
 |-  ( p = <. A , B >. -> ( p e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) )
38 37 3anbi1d 
 |-  ( p = <. A , B >. -> ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) <-> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) ) )
39 breq2 
 |-  ( p = <. A , B >. -> ( <. ( 2nd ` q ) , r >. Cgr p <-> <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) )
40 39 anbi2d 
 |-  ( p = <. A , B >. -> ( ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) <-> ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) )
41 40 riotabidv 
 |-  ( p = <. A , B >. -> ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) )
42 41 eqeq2d 
 |-  ( p = <. A , B >. -> ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) <-> x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) ) )
43 38 42 anbi12d 
 |-  ( p = <. A , B >. -> ( ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) <-> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) ) ) )
44 43 rexbidv 
 |-  ( p = <. A , B >. -> ( E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) ) ) )
45 eleq1 
 |-  ( q = <. C , D >. -> ( q e. ( ( EE ` n ) X. ( EE ` n ) ) <-> <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) ) )
46 fveq2 
 |-  ( q = <. C , D >. -> ( 1st ` q ) = ( 1st ` <. C , D >. ) )
47 fveq2 
 |-  ( q = <. C , D >. -> ( 2nd ` q ) = ( 2nd ` <. C , D >. ) )
48 46 47 neeq12d 
 |-  ( q = <. C , D >. -> ( ( 1st ` q ) =/= ( 2nd ` q ) <-> ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) )
49 45 48 3anbi23d 
 |-  ( q = <. C , D >. -> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) <-> ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) ) )
50 46 opeq1d 
 |-  ( q = <. C , D >. -> <. ( 1st ` q ) , r >. = <. ( 1st ` <. C , D >. ) , r >. )
51 47 50 breq12d 
 |-  ( q = <. C , D >. -> ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. <-> ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. ) )
52 47 opeq1d 
 |-  ( q = <. C , D >. -> <. ( 2nd ` q ) , r >. = <. ( 2nd ` <. C , D >. ) , r >. )
53 52 breq1d 
 |-  ( q = <. C , D >. -> ( <. ( 2nd ` q ) , r >. Cgr <. A , B >. <-> <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) )
54 51 53 anbi12d 
 |-  ( q = <. C , D >. -> ( ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) <-> ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) )
55 54 riotabidv 
 |-  ( q = <. C , D >. -> ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) )
56 55 eqeq2d 
 |-  ( q = <. C , D >. -> ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) <-> x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
57 49 56 anbi12d 
 |-  ( q = <. C , D >. -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) ) <-> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
58 57 rexbidv 
 |-  ( q = <. C , D >. -> ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr <. A , B >. ) ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
59 eqeq1 
 |-  ( x = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) <-> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
60 59 anbi2d 
 |-  ( x = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) <-> ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
61 60 rexbidv 
 |-  ( x = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
62 44 58 61 eloprabg 
 |-  ( ( <. A , B >. e. _V /\ <. C , D >. e. _V /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) e. _V ) -> ( <. <. <. A , B >. , <. C , D >. >. , ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) >. e. { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) } <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) ) )
63 34 35 36 62 mp3an 
 |-  ( <. <. <. A , B >. , <. C , D >. >. , ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) >. e. { <. <. p , q >. , x >. | E. n e. NN ( ( p e. ( ( EE ` n ) X. ( EE ` n ) ) /\ q e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` q ) =/= ( 2nd ` q ) ) /\ x = ( iota_ r e. ( EE ` n ) ( ( 2nd ` q ) Btwn <. ( 1st ` q ) , r >. /\ <. ( 2nd ` q ) , r >. Cgr p ) ) ) } <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
64 31 33 63 3bitri 
 |-  ( <. <. A , B >. , <. C , D >. >. TransportTo ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) <-> E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) )
65 funtransport 
 |-  Fun TransportTo
66 funbrfv 
 |-  ( Fun TransportTo -> ( <. <. A , B >. , <. C , D >. >. TransportTo ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( TransportTo ` <. <. A , B >. , <. C , D >. >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) ) )
67 65 66 ax-mp 
 |-  ( <. <. A , B >. , <. C , D >. >. TransportTo ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( TransportTo ` <. <. A , B >. , <. C , D >. >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )
68 64 67 sylbir 
 |-  ( E. n e. NN ( ( <. A , B >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ <. C , D >. e. ( ( EE ` n ) X. ( EE ` n ) ) /\ ( 1st ` <. C , D >. ) =/= ( 2nd ` <. C , D >. ) ) /\ ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( iota_ r e. ( EE ` n ) ( ( 2nd ` <. C , D >. ) Btwn <. ( 1st ` <. C , D >. ) , r >. /\ <. ( 2nd ` <. C , D >. ) , r >. Cgr <. A , B >. ) ) ) -> ( TransportTo ` <. <. A , B >. , <. C , D >. >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )
69 30 68 syl 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( TransportTo ` <. <. A , B >. , <. C , D >. >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )
70 1 69 syl5eq 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( <. A , B >. TransportTo <. C , D >. ) = ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) )