Metamath Proof Explorer

Theorem sgnsval

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

Ref Expression
Hypotheses sgnsval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
sgnsval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
sgnsval.l ⊢ < = ( lt ‘ 𝑅 )
sgnsval.s ⊢ 𝑆 = ( sgns ‘ 𝑅 )
Assertion sgnsval ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑆 ‘ 𝑋 ) = 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 1 2 3 4 sgnsv ⊢ ( 𝑅 ∈ 𝑉 → 𝑆 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
6 5 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑆 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) ) )
7 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
8 breq2 ⊢ ( 𝑥 = 𝑋 → ( 0 < 𝑥 ↔ 0 < 𝑋 ) )
9 8 ifbid ⊢ ( 𝑥 = 𝑋 → if ( 0 < 𝑥 , 1 , - 1 ) = if ( 0 < 𝑋 , 1 , - 1 ) )
10 7 9 ifbieq2d ⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) = if ( 𝑋 = 0 , 0 , if ( 0 < 𝑋 , 1 , - 1 ) ) )
11 10 adantl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 0 , 0 , if ( 0 < 𝑥 , 1 , - 1 ) ) = if ( 𝑋 = 0 , 0 , if ( 0 < 𝑋 , 1 , - 1 ) ) )
12 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
13 c0ex ⊢ 0 ∈ V
14 13 a1i ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑋 = 0 ) → 0 ∈ V )
15 1ex ⊢ 1 ∈ V
16 15 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑋 = 0 ) ∧ 0 < 𝑋 ) → 1 ∈ V )
17 negex ⊢ - 1 ∈ V
18 17 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑋 = 0 ) ∧ ¬ 0 < 𝑋 ) → - 1 ∈ V )
19 16 18 ifclda ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑋 = 0 ) → if ( 0 < 𝑋 , 1 , - 1 ) ∈ V )
20 14 19 ifclda ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → if ( 𝑋 = 0 , 0 , if ( 0 < 𝑋 , 1 , - 1 ) ) ∈ V )
21 6 11 12 20 fvmptd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑆 ‘ 𝑋 ) = if ( 𝑋 = 0 , 0 , if ( 0 < 𝑋 , 1 , - 1 ) ) )