Metamath Proof Explorer

Theorem mapdhval

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 6-May-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 ) } ) ) ) ) )
mapdh.x 
|- ( ph -> X e. A )
mapdh.f 
|- ( ph -> F e. B )
mapdh.y 
|- ( ph -> Y e. E )
Assertion 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 ) } ) ) ) ) )

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 mapdh.x 
 |-  ( ph -> X e. A )
4 mapdh.f 
 |-  ( ph -> F e. B )
5 mapdh.y 
 |-  ( ph -> Y e. E )
6 otex 
 |-  <. X , F , Y >. e. _V
7 fveq2 
 |-  ( x = <. X , F , Y >. -> ( 2nd ` x ) = ( 2nd ` <. X , F , Y >. ) )
8 7 eqeq1d 
 |-  ( x = <. X , F , Y >. -> ( ( 2nd ` x ) = .0. <-> ( 2nd ` <. X , F , Y >. ) = .0. ) )
9 7 sneqd 
 |-  ( x = <. X , F , Y >. -> { ( 2nd ` x ) } = { ( 2nd ` <. X , F , Y >. ) } )
10 9 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( N ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` <. X , F , Y >. ) } ) )
11 10 fveqeq2d 
 |-  ( x = <. X , F , Y >. -> ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) ) )
12 fveq2 
 |-  ( x = <. X , F , Y >. -> ( 1st ` x ) = ( 1st ` <. X , F , Y >. ) )
13 12 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` <. X , F , Y >. ) ) )
14 13 7 oveq12d 
 |-  ( x = <. X , F , Y >. -> ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) )
15 14 sneqd 
 |-  ( x = <. X , F , Y >. -> { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } )
16 15 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) )
17 16 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) )
18 12 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` <. X , F , Y >. ) ) )
19 18 oveq1d 
 |-  ( x = <. X , F , Y >. -> ( ( 2nd ` ( 1st ` x ) ) R h ) = ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) )
20 19 sneqd 
 |-  ( x = <. X , F , Y >. -> { ( ( 2nd ` ( 1st ` x ) ) R h ) } = { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } )
21 20 fveq2d 
 |-  ( x = <. X , F , Y >. -> ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) )
22 17 21 eqeq12d 
 |-  ( x = <. X , F , Y >. -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) <-> ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) )
23 11 22 anbi12d 
 |-  ( x = <. X , F , Y >. -> ( ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) <-> ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) )
24 23 riotabidv 
 |-  ( x = <. X , F , Y >. -> ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) )
25 8 24 ifbieq2d 
 |-  ( x = <. X , F , Y >. -> 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 ) } ) ) ) ) = if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) )
26 1 fvexi 
 |-  Q e. _V
27 riotaex 
 |-  ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) e. _V
28 26 27 ifex 
 |-  if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) e. _V
29 25 2 28 fvmpt 
 |-  ( <. X , F , Y >. e. _V -> ( I ` <. X , F , Y >. ) = if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) )
30 6 29 mp1i 
 |-  ( ph -> ( I ` <. X , F , Y >. ) = if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) )
31 ot3rdg 
 |-  ( Y e. E -> ( 2nd ` <. X , F , Y >. ) = Y )
32 5 31 syl 
 |-  ( ph -> ( 2nd ` <. X , F , Y >. ) = Y )
33 32 eqeq1d 
 |-  ( ph -> ( ( 2nd ` <. X , F , Y >. ) = .0. <-> Y = .0. ) )
34 32 sneqd 
 |-  ( ph -> { ( 2nd ` <. X , F , Y >. ) } = { Y } )
35 34 fveq2d 
 |-  ( ph -> ( N ` { ( 2nd ` <. X , F , Y >. ) } ) = ( N ` { Y } ) )
36 35 fveqeq2d 
 |-  ( ph -> ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { Y } ) ) = ( J ` { h } ) ) )
37 ot1stg 
 |-  ( ( X e. A /\ F e. B /\ Y e. E ) -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )
38 3 4 5 37 syl3anc 
 |-  ( ph -> ( 1st ` ( 1st ` <. X , F , Y >. ) ) = X )
39 38 32 oveq12d 
 |-  ( ph -> ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) = ( X .- Y ) )
40 39 sneqd 
 |-  ( ph -> { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } = { ( X .- Y ) } )
41 40 fveq2d 
 |-  ( ph -> ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) = ( N ` { ( X .- Y ) } ) )
42 41 fveq2d 
 |-  ( ph -> ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( M ` ( N ` { ( X .- Y ) } ) ) )
43 ot2ndg 
 |-  ( ( X e. A /\ F e. B /\ Y e. E ) -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )
44 3 4 5 43 syl3anc 
 |-  ( ph -> ( 2nd ` ( 1st ` <. X , F , Y >. ) ) = F )
45 44 oveq1d 
 |-  ( ph -> ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) = ( F R h ) )
46 45 sneqd 
 |-  ( ph -> { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } = { ( F R h ) } )
47 46 fveq2d 
 |-  ( ph -> ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) = ( J ` { ( F R h ) } ) )
48 42 47 eqeq12d 
 |-  ( ph -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) <-> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) )
49 36 48 anbi12d 
 |-  ( ph -> ( ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) <-> ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
50 49 riotabidv 
 |-  ( ph -> ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) )
51 33 50 ifbieq2d 
 |-  ( ph -> if ( ( 2nd ` <. X , F , Y >. ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` <. X , F , Y >. ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` <. X , F , Y >. ) ) .- ( 2nd ` <. X , F , Y >. ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` <. X , F , Y >. ) ) R h ) } ) ) ) ) = if ( Y = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) )
52 30 51 eqtrd 
 |-  ( 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 ) } ) ) ) ) )