Theorem sgnsv

Description: The sign mapping. (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	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)$$

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		elex	$$⊢R\in V\to R\in \mathrm{V}$$
6		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
7	6 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
8		fveq2	$$⊢r=R\to 0_r=0_R$$
9	8 2	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
10	9	adantr	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to 0_r=\underset{\dot{}}{0}$$
11	10	eqeq2d	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to \left(x=0_r\leftrightarrow x=\underset{\dot{}}{0}\right)$$
12		fveq2	$$⊢r=R\to {<}_r={<}_R$$
13	12 3	eqtr4di	$$⊢r=R\to {<}_r=\underset{\dot{}}{<}$$
14	13	adantr	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to {<}_r=\underset{\dot{}}{<}$$
15		eqidd	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to x=x$$
16	10 14 15	breq123d	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to \left(0_r{<}_{r}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}x\right)$$
17	16	ifbid	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to if\left(0_r{<}_{r}x,1,-1\right)=if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)$$
18	11 17	ifbieq2d	$$⊢\left(r=R\wedge x\in {\mathrm{Base}}_r\right)\to if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)=if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)$$
19	7 18	mpteq12dva	$$⊢r=R\to \left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
20		df-sgns	$$⊢{sgn}_s=\left(r\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_r⟼if\left(x=0_r,0,if\left(0_r{<}_{r}x,1,-1\right)\right)\right)\right)$$
21	19 20 1	mptfvmpt	$$⊢R\in \mathrm{V}\to {sgn}_s\left(R\right)=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
22	5 21	syl	$$⊢R\in V\to {sgn}_s\left(R\right)=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,if\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x,1,-1\right)\right)\right)$$
23	4 22	eqtrid	$$⊢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)$$