Metamath Proof Explorer

Theorem mapdhval2

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015)

Ref Expression
Hypotheses mapdh.q 
|- Q = ( 0g ` C )
mapdh.i 
|- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
mapdh2.x 
|- ( ph -> X e. A )
mapdh2.f 
|- ( ph -> F e. B )
mapdh2.y 
|- ( ph -> Y e. ( V \ { .0. } ) )
Assertion mapdhval2 
|- ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 mapdh.q 
 |-  Q = ( 0g ` C )
2 mapdh.i 
 |-  I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )
3 mapdh2.x 
 |-  ( ph -> X e. A )
4 mapdh2.f 
 |-  ( ph -> F e. B )
5 mapdh2.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
6 1 2 3 4 5 mapdhval 
 |-  ( ph -> ( I ` <. X , F , Y >. ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
7 eldifsni 
 |-  ( Y e. ( V \ { .0. } ) -> Y =/= .0. )
8 7 neneqd 
 |-  ( Y e. ( V \ { .0. } ) -> -. Y = .0. )
9 iffalse 
 |-  ( -. Y = .0. -> if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
10 5 8 9 3syl 
 |-  ( ph -> if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
11 6 10 eqtrd 
 |-  ( ph -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )