Theorem sgnsv

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

	Ref	Expression
Hypotheses	sgnsval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	sgnsval.0	⊢ 0 = ( 0g ‘ 𝑅 )
	sgnsval.l	⊢ < = ( lt ‘ 𝑅 )
	sgnsval.s	⊢ 𝑆 = ( sgns ‘ 𝑅 )
Assertion	sgnsv	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sgnsval.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		sgnsval.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		sgnsval.l	⊢ < = ( lt ‘ 𝑅 )
4		sgnsval.s	⊢ 𝑆 = ( sgns ‘ 𝑅 )
5		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7	6 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
9	8 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
10	9	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → ( 0g ‘ 𝑟 ) = 0 )
11	10	eqeq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → ( 𝑥 = ( 0g ‘ 𝑟 ) ↔ 𝑥 = 0 ) )
12		fveq2	⊢ ( 𝑟 = 𝑅 → ( lt ‘ 𝑟 ) = ( lt ‘ 𝑅 ) )
13	12 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( lt ‘ 𝑟 ) = < )
14	13	adantr	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → ( lt ‘ 𝑟 ) = < )
15		eqidd	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → 𝑥 = 𝑥 )
16	10 14 15	breq123d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 ↔ 0 < 𝑥 ) )
17	16	ifbid	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) = if ( 0 < 𝑥 , 1 , - 1 ) )
18	11 17	ifbieq2d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑥 ∈ ( Base ‘ 𝑟 ) ) → if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) = if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) )
19	7 18	mpteq12dva	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
20		df-sgns	⊢ sgns = ( 𝑟 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ if ( 𝑥 = ( 0g ‘ 𝑟 ) , 0 , if ( ( 0g ‘ 𝑟 ) ( lt ‘ 𝑟 ) 𝑥 , 1 , - 1 ) ) ) )
21	19 20 1	mptfvmpt	⊢ ( 𝑅 ∈ V → ( sgns ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
22	5 21	syl	⊢ ( 𝑅 ∈ 𝑉 → ( sgns ‘ 𝑅 ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
23	4 22	eqtrid	⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )