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 | chil 27160 | . . 3 class ℋ | |
3 | 1, 2 | wcel 1977 | . 2 wff 𝐴 ∈ ℋ |
4 | c1 9816 | . . . 4 class 1 | |
5 | csm 27162 | . . . 4 class ·ℎ | |
6 | 4, 1, 5 | co 6549 | . . 3 class (1 ·ℎ 𝐴) |
7 | 6, 1 | wceq 1475 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 27266 hvsubid 27267 hvaddsubval 27274 hv2times 27302 hvnegdii 27303 hilvc 27403 hhssnv 27505 h1de2bi 27797 h1datomi 27824 mayete3i 27971 homulid2 28043 lnop0 28209 lnopaddi 28214 lnophmlem2 28260 lnfn0i 28285 lnfnaddi 28286 strlem1 28493 |
Copyright terms: Public domain | W3C validator |