Metamath Proof Explorer

Theorem hdmap1cbv

Description: Frequently used lemma to change bound variables in L hypothesis. (Contributed by NM, 15-May-2015)

Ref Expression
Hypothesis hdmap1cbv.l 
|- L = ( 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 ) } ) ) ) ) )
Assertion hdmap1cbv 
|- L = ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hdmap1cbv.l 
 |-  L = ( 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 ) } ) ) ) ) )
2 fveq2 
 |-  ( x = y -> ( 2nd ` x ) = ( 2nd ` y ) )
3 2 eqeq1d 
 |-  ( x = y -> ( ( 2nd ` x ) = .0. <-> ( 2nd ` y ) = .0. ) )
4 2 sneqd 
 |-  ( x = y -> { ( 2nd ` x ) } = { ( 2nd ` y ) } )
5 4 fveq2d 
 |-  ( x = y -> ( N ` { ( 2nd ` x ) } ) = ( N ` { ( 2nd ` y ) } ) )
6 5 fveq2d 
 |-  ( x = y -> ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( M ` ( N ` { ( 2nd ` y ) } ) ) )
7 6 eqeq1d 
 |-  ( x = y -> ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) ) )
8 2fveq3 
 |-  ( x = y -> ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) )
9 8 2 oveq12d 
 |-  ( x = y -> ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) = ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) )
10 9 sneqd 
 |-  ( x = y -> { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } = { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } )
11 10 fveq2d 
 |-  ( x = y -> ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) = ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) )
12 11 fveq2d 
 |-  ( x = y -> ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) )
13 2fveq3 
 |-  ( x = y -> ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) )
14 13 oveq1d 
 |-  ( x = y -> ( ( 2nd ` ( 1st ` x ) ) R h ) = ( ( 2nd ` ( 1st ` y ) ) R h ) )
15 14 sneqd 
 |-  ( x = y -> { ( ( 2nd ` ( 1st ` x ) ) R h ) } = { ( ( 2nd ` ( 1st ` y ) ) R h ) } )
16 15 fveq2d 
 |-  ( x = y -> ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) )
17 12 16 eqeq12d 
 |-  ( x = y -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) <-> ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) )
18 7 17 anbi12d 
 |-  ( x = y -> ( ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) <-> ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) )
19 18 riotabidv 
 |-  ( x = 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 ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) )
20 3 19 ifbieq2d 
 |-  ( x = 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 ` y ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) ) )
21 20 cbvmptv 
 |-  ( 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 ) } ) ) ) ) ) = ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) ) )
22 sneq 
 |-  ( h = i -> { h } = { i } )
23 22 fveq2d 
 |-  ( h = i -> ( J ` { h } ) = ( J ` { i } ) )
24 23 eqeq2d 
 |-  ( h = i -> ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) <-> ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) ) )
25 oveq2 
 |-  ( h = i -> ( ( 2nd ` ( 1st ` y ) ) R h ) = ( ( 2nd ` ( 1st ` y ) ) R i ) )
26 25 sneqd 
 |-  ( h = i -> { ( ( 2nd ` ( 1st ` y ) ) R h ) } = { ( ( 2nd ` ( 1st ` y ) ) R i ) } )
27 26 fveq2d 
 |-  ( h = i -> ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) )
28 27 eqeq2d 
 |-  ( h = i -> ( ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) <-> ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) )
29 24 28 anbi12d 
 |-  ( h = i -> ( ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) <-> ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) )
30 29 cbvriotavw 
 |-  ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) = ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) )
31 ifeq2 
 |-  ( ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) = ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) -> if ( ( 2nd ` y ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) ) = if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) )
32 30 31 ax-mp 
 |-  if ( ( 2nd ` y ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) ) = if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) )
33 32 mpteq2i 
 |-  ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R h ) } ) ) ) ) ) = ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) )
34 1 21 33 3eqtri 
 |-  L = ( y e. _V |-> if ( ( 2nd ` y ) = .0. , Q , ( iota_ i e. D ( ( M ` ( N ` { ( 2nd ` y ) } ) ) = ( J ` { i } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` y ) ) .- ( 2nd ` y ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` y ) ) R i ) } ) ) ) ) )