Metamath Proof Explorer

Theorem transportprops

Description: Calculate the defining properties of the transport function. (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 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 >. ) ) )
2 1 eqcomd 
 |-  ( ( N e. NN /\ ( ( 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 >. ) ) = ( <. A , B >. TransportTo <. C , D >. ) )
3 transportcl 
 |-  ( ( 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 >. ) e. ( EE ` N ) )
4 segconeu 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) )
5 opeq2 
 |-  ( r = ( <. A , B >. TransportTo <. C , D >. ) -> <. C , r >. = <. C , ( <. A , B >. TransportTo <. C , D >. ) >. )
6 5 breq2d 
 |-  ( r = ( <. A , B >. TransportTo <. C , D >. ) -> ( D Btwn <. C , r >. <-> D Btwn <. C , ( <. A , B >. TransportTo <. C , D >. ) >. ) )
7 opeq2 
 |-  ( r = ( <. A , B >. TransportTo <. C , D >. ) -> <. D , r >. = <. D , ( <. A , B >. TransportTo <. C , D >. ) >. )
8 7 breq1d 
 |-  ( r = ( <. A , B >. TransportTo <. C , D >. ) -> ( <. D , r >. Cgr <. A , B >. <-> <. D , ( <. A , B >. TransportTo <. C , D >. ) >. Cgr <. A , B >. ) )
9 6 8 anbi12d 
 |-  ( r = ( <. A , B >. TransportTo <. C , D >. ) -> ( ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) <-> ( D Btwn <. C , ( <. A , B >. TransportTo <. C , D >. ) >. /\ <. D , ( <. A , B >. TransportTo <. C , D >. ) >. Cgr <. A , B >. ) ) )
10 9 riota2 
 |-  ( ( ( <. A , B >. TransportTo <. C , D >. ) e. ( EE ` N ) /\ E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) -> ( ( D Btwn <. C , ( <. A , B >. TransportTo <. C , D >. ) >. /\ <. D , ( <. A , B >. TransportTo <. C , D >. ) >. Cgr <. A , B >. ) <-> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( <. A , B >. TransportTo <. C , D >. ) ) )
11 3 4 10 syl2anc 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( ( D Btwn <. C , ( <. A , B >. TransportTo <. C , D >. ) >. /\ <. D , ( <. A , B >. TransportTo <. C , D >. ) >. Cgr <. A , B >. ) <-> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) = ( <. A , B >. TransportTo <. C , D >. ) ) )
12 2 11 mpbird 
 |-  ( ( N e. NN /\ ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ C =/= D ) ) -> ( D Btwn <. C , ( <. A , B >. TransportTo <. C , D >. ) >. /\ <. D , ( <. A , B >. TransportTo <. C , D >. ) >. Cgr <. A , B >. ) )