![]() |
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 28116 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2145 | . 2 wff 𝐴 ∈ ℋ |
4 | c1 10139 | . . . 4 class 1 | |
5 | csm 28118 | . . . 4 class ·ℎ | |
6 | 4, 1, 5 | co 6793 | . . 3 class (1 ·ℎ 𝐴) |
7 | 6, 1 | wceq 1631 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 28222 hvsubid 28223 hvaddsubval 28230 hv2times 28258 hvnegdii 28259 hilvc 28359 hhssnv 28461 h1de2bi 28753 h1datomi 28780 mayete3i 28927 homulid2 28999 lnop0 29165 lnopaddi 29170 lnophmlem2 29216 lnfn0i 29241 lnfnaddi 29242 strlem1 29449 |
Copyright terms: Public domain | W3C validator |