Metamath Proof Explorer

Theorem transportcl

Description: Closure law for segment transport. (Contributed by Scott Fenton, 19-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion 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 ) )

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 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 >. ) )
3 riotacl 
 |-  ( E! r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) -> ( iota_ r e. ( EE ` N ) ( D Btwn <. C , r >. /\ <. D , r >. Cgr <. A , B >. ) ) e. ( EE ` N ) )
4 2 3 syl 
 |-  ( ( 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 >. ) ) e. ( EE ` N ) )
5 1 4 eqeltrd 
 |-  ( ( 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 ) )