Metamath Proof Explorer

Theorem fvmptnn04ifb

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the second case. (Contributed by AV, 10-Nov-2019)

Ref Expression
Hypotheses fvmptnn04if.g 
|- G = ( n e. NN0 |-> if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
fvmptnn04if.s 
|- ( ph -> S e. NN )
fvmptnn04if.n 
|- ( ph -> N e. NN0 )
Assertion fvmptnn04ifb 
|- ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> ( G ` N ) = [_ N / n ]_ B )

Proof

Step Hyp Ref Expression
1 fvmptnn04if.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , A , if ( n = S , C , if ( S < n , D , B ) ) ) )
2 fvmptnn04if.s 
 |-  ( ph -> S e. NN )
3 fvmptnn04if.n 
 |-  ( ph -> N e. NN0 )
4 2 3ad2ant1 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> S e. NN )
5 3 3ad2ant1 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> N e. NN0 )
6 simp3 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> [_ N / n ]_ B e. V )
7 nn0re 
 |-  ( N e. NN0 -> N e. RR )
8 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
9 7 8 jca 
 |-  ( N e. NN0 -> ( N e. RR /\ 0 <_ N ) )
10 ne0gt0 
 |-  ( ( N e. RR /\ 0 <_ N ) -> ( N =/= 0 <-> 0 < N ) )
11 3 9 10 3syl 
 |-  ( ph -> ( N =/= 0 <-> 0 < N ) )
12 11 biimprcd 
 |-  ( 0 < N -> ( ph -> N =/= 0 ) )
13 12 adantr 
 |-  ( ( 0 < N /\ N < S ) -> ( ph -> N =/= 0 ) )
14 13 impcom 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) ) -> N =/= 0 )
15 14 3adant3 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> N =/= 0 )
16 neneq 
 |-  ( N =/= 0 -> -. N = 0 )
17 16 pm2.21d 
 |-  ( N =/= 0 -> ( N = 0 -> [_ N / n ]_ B = [_ N / n ]_ A ) )
18 15 17 syl 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> ( N = 0 -> [_ N / n ]_ B = [_ N / n ]_ A ) )
19 18 imp 
 |-  ( ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) /\ N = 0 ) -> [_ N / n ]_ B = [_ N / n ]_ A )
20 eqidd 
 |-  ( ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) /\ 0 < N /\ N < S ) -> [_ N / n ]_ B = [_ N / n ]_ B )
21 3 7 syl 
 |-  ( ph -> N e. RR )
22 21 adantr 
 |-  ( ( ph /\ N < S ) -> N e. RR )
23 simpr 
 |-  ( ( ph /\ N < S ) -> N < S )
24 22 23 ltned 
 |-  ( ( ph /\ N < S ) -> N =/= S )
25 24 neneqd 
 |-  ( ( ph /\ N < S ) -> -. N = S )
26 25 adantrl 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) ) -> -. N = S )
27 26 3adant3 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> -. N = S )
28 27 pm2.21d 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> ( N = S -> [_ N / n ]_ B = [_ N / n ]_ C ) )
29 28 imp 
 |-  ( ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) /\ N = S ) -> [_ N / n ]_ B = [_ N / n ]_ C )
30 2 nnred 
 |-  ( ph -> S e. RR )
31 ltnsym 
 |-  ( ( N e. RR /\ S e. RR ) -> ( N < S -> -. S < N ) )
32 21 30 31 syl2anc 
 |-  ( ph -> ( N < S -> -. S < N ) )
33 32 com12 
 |-  ( N < S -> ( ph -> -. S < N ) )
34 33 adantl 
 |-  ( ( 0 < N /\ N < S ) -> ( ph -> -. S < N ) )
35 34 impcom 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) ) -> -. S < N )
36 35 3adant3 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> -. S < N )
37 36 pm2.21d 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> ( S < N -> [_ N / n ]_ B = [_ N / n ]_ D ) )
38 37 imp 
 |-  ( ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) /\ S < N ) -> [_ N / n ]_ B = [_ N / n ]_ D )
39 1 4 5 6 19 20 29 38 fvmptnn04if 
 |-  ( ( ph /\ ( 0 < N /\ N < S ) /\ [_ N / n ]_ B e. V ) -> ( G ` N ) = [_ N / n ]_ B )