Metamath Proof Explorer


Theorem fvmptnn04ifd

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

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