Description: Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax-xrsvsca | ⊢ ·e = ( ·𝑠 ‘ ℝ*𝑠 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cxmu | ⊢ ·e | |
| 1 | cvsca | ⊢ ·𝑠 | |
| 2 | cxrs | ⊢ ℝ*𝑠 | |
| 3 | 2 1 | cfv | ⊢ ( ·𝑠 ‘ ℝ*𝑠 ) |
| 4 | 0 3 | wceq | ⊢ ·e = ( ·𝑠 ‘ ℝ*𝑠 ) |