# Metamath Proof Explorer

## Theorem sgnsf

Description: The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018)

Ref Expression
Hypotheses sgnsval.b
`|- B = ( Base ` R )`
sgnsval.0
`|- .0. = ( 0g ` R )`
sgnsval.l
`|- .< = ( lt ` R )`
sgnsval.s
`|- S = ( sgns ` R )`
Assertion sgnsf
`|- ( R e. V -> S : B --> { -u 1 , 0 , 1 } )`

### Proof

Step Hyp Ref Expression
1 sgnsval.b
` |-  B = ( Base ` R )`
2 sgnsval.0
` |-  .0. = ( 0g ` R )`
3 sgnsval.l
` |-  .< = ( lt ` R )`
4 sgnsval.s
` |-  S = ( sgns ` R )`
5 1 2 3 4 sgnsv
` |-  ( R e. V -> S = ( x e. B |-> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) ) )`
6 c0ex
` |-  0 e. _V`
7 6 tpid2
` |-  0 e. { -u 1 , 0 , 1 }`
8 1ex
` |-  1 e. _V`
9 8 tpid3
` |-  1 e. { -u 1 , 0 , 1 }`
10 negex
` |-  -u 1 e. _V`
11 10 tpid1
` |-  -u 1 e. { -u 1 , 0 , 1 }`
12 9 11 ifcli
` |-  if ( .0. .< x , 1 , -u 1 ) e. { -u 1 , 0 , 1 }`
13 7 12 ifcli
` |-  if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) e. { -u 1 , 0 , 1 }`
14 13 a1i
` |-  ( ( R e. V /\ x e. B ) -> if ( x = .0. , 0 , if ( .0. .< x , 1 , -u 1 ) ) e. { -u 1 , 0 , 1 } )`
15 5 14 fmpt3d
` |-  ( R e. V -> S : B --> { -u 1 , 0 , 1 } )`