![]() |
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 30035 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2106 | . 2 wff 𝐴 ∈ ℋ |
4 | c1 11093 | . . . 4 class 1 | |
5 | csm 30037 | . . . 4 class ·ℎ | |
6 | 4, 1, 5 | co 7393 | . . 3 class (1 ·ℎ 𝐴) |
7 | 6, 1 | wceq 1541 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 30141 hvsubid 30142 hvaddsubval 30149 hv2times 30177 hvnegdii 30178 hilvc 30278 hhssnv 30380 h1de2bi 30670 h1datomi 30697 mayete3i 30844 homullid 30916 lnop0 31082 lnopaddi 31087 lnophmlem2 31133 lnfn0i 31158 lnfnaddi 31159 strlem1 31366 |
Copyright terms: Public domain | W3C validator |