Metamath Proof Explorer

Theorem fvmptnn04ifa

Description: The function value of a mapping from the nonnegative integers with four distinct cases for the first 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 fvmptnn04ifa 
|- ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> ( G ` N ) = [_ N / n ]_ A )

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 /\ N = 0 /\ [_ N / n ]_ A e. V ) -> S e. NN )
5 3 3ad2ant1 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> N e. NN0 )
6 simp3 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> [_ N / n ]_ A e. V )
7 eqidd 
 |-  ( ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) /\ N = 0 ) -> [_ N / n ]_ A = [_ N / n ]_ A )
8 simpr 
 |-  ( ( ph /\ 0 < N ) -> 0 < N )
9 8 gt0ne0d 
 |-  ( ( ph /\ 0 < N ) -> N =/= 0 )
10 9 neneqd 
 |-  ( ( ph /\ 0 < N ) -> -. N = 0 )
11 10 pm2.21d 
 |-  ( ( ph /\ 0 < N ) -> ( N = 0 -> ( N < S -> [_ N / n ]_ A = [_ N / n ]_ B ) ) )
12 11 impancom 
 |-  ( ( ph /\ N = 0 ) -> ( 0 < N -> ( N < S -> [_ N / n ]_ A = [_ N / n ]_ B ) ) )
13 12 3adant3 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> ( 0 < N -> ( N < S -> [_ N / n ]_ A = [_ N / n ]_ B ) ) )
14 13 3imp 
 |-  ( ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) /\ 0 < N /\ N < S ) -> [_ N / n ]_ A = [_ N / n ]_ B )
15 2 nnne0d 
 |-  ( ph -> S =/= 0 )
16 15 necomd 
 |-  ( ph -> 0 =/= S )
17 16 adantr 
 |-  ( ( ph /\ N = 0 ) -> 0 =/= S )
18 neeq1 
 |-  ( N = 0 -> ( N =/= S <-> 0 =/= S ) )
19 18 adantl 
 |-  ( ( ph /\ N = 0 ) -> ( N =/= S <-> 0 =/= S ) )
20 17 19 mpbird 
 |-  ( ( ph /\ N = 0 ) -> N =/= S )
21 20 3adant3 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> N =/= S )
22 21 neneqd 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> -. N = S )
23 22 pm2.21d 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> ( N = S -> [_ N / n ]_ A = [_ N / n ]_ C ) )
24 23 imp 
 |-  ( ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) /\ N = S ) -> [_ N / n ]_ A = [_ N / n ]_ C )
25 nnnn0 
 |-  ( S e. NN -> S e. NN0 )
26 nn0nlt0 
 |-  ( S e. NN0 -> -. S < 0 )
27 2 25 26 3syl 
 |-  ( ph -> -. S < 0 )
28 27 adantr 
 |-  ( ( ph /\ N = 0 ) -> -. S < 0 )
29 breq2 
 |-  ( N = 0 -> ( S < N <-> S < 0 ) )
30 29 notbid 
 |-  ( N = 0 -> ( -. S < N <-> -. S < 0 ) )
31 30 adantl 
 |-  ( ( ph /\ N = 0 ) -> ( -. S < N <-> -. S < 0 ) )
32 28 31 mpbird 
 |-  ( ( ph /\ N = 0 ) -> -. S < N )
33 32 3adant3 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> -. S < N )
34 33 pm2.21d 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> ( S < N -> [_ N / n ]_ A = [_ N / n ]_ D ) )
35 34 imp 
 |-  ( ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) /\ S < N ) -> [_ N / n ]_ A = [_ N / n ]_ D )
36 1 4 5 6 7 14 24 35 fvmptnn04if 
 |-  ( ( ph /\ N = 0 /\ [_ N / n ]_ A e. V ) -> ( G ` N ) = [_ N / n ]_ A )