Metamath Proof Explorer


Theorem sgnsv

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

Ref Expression
Hypotheses sgnsval.b B = Base R
sgnsval.0 0 ˙ = 0 R
sgnsval.l < ˙ = < R
sgnsval.s S = sgn s R
Assertion sgnsv R V S = x B if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1

Proof

Step Hyp Ref Expression
1 sgnsval.b B = Base R
2 sgnsval.0 0 ˙ = 0 R
3 sgnsval.l < ˙ = < R
4 sgnsval.s S = sgn s R
5 elex R V R V
6 fveq2 r = R Base r = Base R
7 6 1 syl6eqr r = R Base r = B
8 fveq2 r = R 0 r = 0 R
9 8 2 syl6eqr r = R 0 r = 0 ˙
10 9 adantr r = R x Base r 0 r = 0 ˙
11 10 eqeq2d r = R x Base r x = 0 r x = 0 ˙
12 fveq2 r = R < r = < R
13 12 3 syl6eqr r = R < r = < ˙
14 13 adantr r = R x Base r < r = < ˙
15 eqidd r = R x Base r x = x
16 10 14 15 breq123d r = R x Base r 0 r < r x 0 ˙ < ˙ x
17 16 ifbid r = R x Base r if 0 r < r x 1 1 = if 0 ˙ < ˙ x 1 1
18 11 17 ifbieq2d r = R x Base r if x = 0 r 0 if 0 r < r x 1 1 = if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1
19 7 18 mpteq12dva r = R x Base r if x = 0 r 0 if 0 r < r x 1 1 = x B if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1
20 df-sgns sgn s = r V x Base r if x = 0 r 0 if 0 r < r x 1 1
21 19 20 1 mptfvmpt R V sgn s R = x B if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1
22 5 21 syl R V sgn s R = x B if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1
23 4 22 syl5eq R V S = x B if x = 0 ˙ 0 if 0 ˙ < ˙ x 1 1