Metamath Proof Explorer

Theorem fvmptnn04ifc

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

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 = S /\ [_ N / n ]_ C e. V ) -> S e. NN )
5 3 3ad2ant1 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> N e. NN0 )
6 simp3 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> [_ N / n ]_ C e. V )
7 nnne0 
 |-  ( S e. NN -> S =/= 0 )
8 7 neneqd 
 |-  ( S e. NN -> -. S = 0 )
9 2 8 syl 
 |-  ( ph -> -. S = 0 )
10 9 adantr 
 |-  ( ( ph /\ N = S ) -> -. S = 0 )
11 eqeq1 
 |-  ( N = S -> ( N = 0 <-> S = 0 ) )
12 11 notbid 
 |-  ( N = S -> ( -. N = 0 <-> -. S = 0 ) )
13 12 adantl 
 |-  ( ( ph /\ N = S ) -> ( -. N = 0 <-> -. S = 0 ) )
14 10 13 mpbird 
 |-  ( ( ph /\ N = S ) -> -. N = 0 )
15 14 3adant3 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> -. N = 0 )
16 15 pm2.21d 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> ( N = 0 -> [_ N / n ]_ C = [_ N / n ]_ A ) )
17 16 imp 
 |-  ( ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) /\ N = 0 ) -> [_ N / n ]_ C = [_ N / n ]_ A )
18 3 nn0red 
 |-  ( ph -> N e. RR )
19 2 nnred 
 |-  ( ph -> S e. RR )
20 18 19 lttri3d 
 |-  ( ph -> ( N = S <-> ( -. N < S /\ -. S < N ) ) )
21 20 simprbda 
 |-  ( ( ph /\ N = S ) -> -. N < S )
22 21 pm2.21d 
 |-  ( ( ph /\ N = S ) -> ( N < S -> [_ N / n ]_ C = [_ N / n ]_ B ) )
23 22 3adant3 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> ( N < S -> [_ N / n ]_ C = [_ N / n ]_ B ) )
24 23 a1d 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> ( 0 < N -> ( N < S -> [_ N / n ]_ C = [_ N / n ]_ B ) ) )
25 24 3imp 
 |-  ( ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) /\ 0 < N /\ N < S ) -> [_ N / n ]_ C = [_ N / n ]_ B )
26 eqidd 
 |-  ( ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) /\ N = S ) -> [_ N / n ]_ C = [_ N / n ]_ C )
27 20 simplbda 
 |-  ( ( ph /\ N = S ) -> -. S < N )
28 27 3adant3 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> -. S < N )
29 28 pm2.21d 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> ( S < N -> [_ N / n ]_ C = [_ N / n ]_ D ) )
30 29 imp 
 |-  ( ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) /\ S < N ) -> [_ N / n ]_ C = [_ N / n ]_ D )
31 1 4 5 6 17 25 26 30 fvmptnn04if 
 |-  ( ( ph /\ N = S /\ [_ N / n ]_ C e. V ) -> ( G ` N ) = [_ N / n ]_ C )