Description: If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | scaffval.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| scaffval.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | ||
| scaffval.k | ⊢ 𝐾 = ( Base ‘ 𝐹 ) | ||
| scaffval.a | ⊢ ∙ = ( ·sf ‘ 𝑊 ) | ||
| scaffval.s | ⊢ · = ( ·𝑠 ‘ 𝑊 ) | ||
| Assertion | scafeq | ⊢ ( · Fn ( 𝐾 × 𝐵 ) → ∙ = · ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | scaffval.b | ⊢ 𝐵 = ( Base ‘ 𝑊 ) | |
| 2 | scaffval.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
| 3 | scaffval.k | ⊢ 𝐾 = ( Base ‘ 𝐹 ) | |
| 4 | scaffval.a | ⊢ ∙ = ( ·sf ‘ 𝑊 ) | |
| 5 | scaffval.s | ⊢ · = ( ·𝑠 ‘ 𝑊 ) | |
| 6 | 1 2 3 4 5 | scaffval | ⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) |
| 7 | fnov | ⊢ ( · Fn ( 𝐾 × 𝐵 ) ↔ · = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) ) | |
| 8 | 7 | biimpi | ⊢ ( · Fn ( 𝐾 × 𝐵 ) → · = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 · 𝑦 ) ) ) |
| 9 | 6 8 | eqtr4id | ⊢ ( · Fn ( 𝐾 × 𝐵 ) → ∙ = · ) |