| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > ax-hvmulid | Structured version Visualization version GIF version | ||
| Description: Scalar multiplication by one. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-hvmulid | ⊢ (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | chba 30938 | . . 3 class ℋ | |
| 3 | 1, 2 | wcel 2108 | . 2 wff 𝐴 ∈ ℋ |
| 4 | c1 11156 | . . . 4 class 1 | |
| 5 | csm 30940 | . . . 4 class ·ℎ | |
| 6 | 4, 1, 5 | co 7431 | . . 3 class (1 ·ℎ 𝐴) |
| 7 | 6, 1 | wceq 1540 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
| 8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: hvmul0or 31044 hvsubid 31045 hvaddsubval 31052 hv2times 31080 hvnegdii 31081 hilvc 31181 hhssnv 31283 h1de2bi 31573 h1datomi 31600 mayete3i 31747 homullid 31819 lnop0 31985 lnopaddi 31990 lnophmlem2 32036 lnfn0i 32061 lnfnaddi 32062 strlem1 32269 |
| Copyright terms: Public domain | W3C validator |