Step | Hyp | Ref
| Expression |
1 | | sgnsval.s |
. 2
⊢ 𝑆 = (sgns‘𝑅) |
2 | | elex 3185 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
4 | | sgnsval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
5 | 3, 4 | syl6eqr 2662 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
6 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = (0g‘𝑅)) |
7 | | sgnsval.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (0g‘𝑟) = 0 ) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → (0g‘𝑟) = 0 ) |
10 | 9 | eqeq2d 2620 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → (𝑥 = (0g‘𝑟) ↔ 𝑥 = 0 )) |
11 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (lt‘𝑟) = (lt‘𝑅)) |
12 | | sgnsval.l |
. . . . . . . . . 10
⊢ < =
(lt‘𝑅) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (lt‘𝑟) = < ) |
14 | 13 | adantr 480 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → (lt‘𝑟) = < ) |
15 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → 𝑥 = 𝑥) |
16 | 9, 14, 15 | breq123d 4597 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → ((0g‘𝑟)(lt‘𝑟)𝑥 ↔ 0 < 𝑥)) |
17 | 16 | ifbid 4058 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1) = if( 0 < 𝑥, 1, -1)) |
18 | 10, 17 | ifbieq2d 4061 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑥 ∈ (Base‘𝑟)) → if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)) = if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1))) |
19 | 5, 18 | mpteq12dva 4662 |
. . . 4
⊢ (𝑟 = 𝑅 → (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))) = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1)))) |
20 | | df-sgns 29057 |
. . . 4
⊢
sgns = (𝑟
∈ V ↦ (𝑥 ∈
(Base‘𝑟) ↦
if(𝑥 =
(0g‘𝑟), 0,
if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1)))) |
21 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑟)
∈ V |
22 | 21 | mptex 6390 |
. . . 4
⊢ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))) ∈ V |
23 | 19, 20, 22 | fvmpt3i 6196 |
. . 3
⊢ (𝑅 ∈ V →
(sgns‘𝑅) =
(𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1)))) |
24 | 2, 23 | syl 17 |
. 2
⊢ (𝑅 ∈ 𝑉 → (sgns‘𝑅) = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1)))) |
25 | 1, 24 | syl5eq 2656 |
1
⊢ (𝑅 ∈ 𝑉 → 𝑆 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1)))) |