Theorem sgnsval

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

	Ref	Expression
Hypotheses	sgnsval.b	$$⊢B={\mathrm{Base}}_R$$
	sgnsval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	sgnsval.l	$$⊢\underset{\dot{}}{<}={<}_R$$
	sgnsval.s	$$⊢S={sgn}_s\left(R\right)$$
Assertion	sgnsval	$$⊢\left(R\in V\wedge X\in B\right)\to S\left(X\right)=if\left(X=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sgnsval.b	$$⊢B={\mathrm{Base}}_R$$
2		sgnsval.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		sgnsval.l	$$⊢\underset{\dot{}}{<}={<}_R$$
4		sgnsval.s	$$⊢S={sgn}_s\left(R\right)$$
5	1 2 3 4	sgnsv	$$⊢R\in V\to S=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
6	5	adantr	$$⊢\left(R\in V\wedge X\in B\right)\to S=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
7		eqeq1	$$⊢x=X\to \left(x=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
8		breq2	$$⊢x=X\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)$$
9	8	ifbid	$$⊢x=X\to if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)=if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)$$
10	7 9	ifbieq2d	$$⊢x=X\to if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)=if\left(X=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\right)$$
11	10	adantl	$$⊢\left(\left(R\in V\wedge X\in B\right)\wedge x=X\right)\to if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)=if\left(X=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\right)$$
12		simpr	$$⊢\left(R\in V\wedge X\in B\right)\to X\in B$$
13		c0ex	$$⊢0\in \mathrm{V}$$
14	13	a1i	$$⊢\left(\left(R\in V\wedge X\in B\right)\wedge X=\underset{\dot{}}{0}\right)\to 0\in \mathrm{V}$$
15		1ex	$$⊢1\in \mathrm{V}$$
16	15	a1i	$$⊢\left(\left(\left(R\in V\wedge X\in B\right)\wedge \neg X=\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to 1\in \mathrm{V}$$
17		negex	$$⊢-1\in \mathrm{V}$$
18	17	a1i	$$⊢\left(\left(\left(R\in V\wedge X\in B\right)\wedge \neg X=\underset{\dot{}}{0}\right)\wedge \neg \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)\to -1\in \mathrm{V}$$
19	16 18	ifclda	$$⊢\left(\left(R\in V\wedge X\in B\right)\wedge \neg X=\underset{\dot{}}{0}\right)\to if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\in \mathrm{V}$$
20	14 19	ifclda	$$⊢\left(R\in V\wedge X\in B\right)\to if\left(X=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\right)\in \mathrm{V}$$
21	6 11 12 20	fvmptd	$$⊢\left(R\in V\wedge X\in B\right)\to S\left(X\right)=if\left(X=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X,1,-1\right)\right)$$