![]() |
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 28387 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2081 | . 2 wff 𝐴 ∈ ℋ |
4 | c1 10384 | . . . 4 class 1 | |
5 | csm 28389 | . . . 4 class ·ℎ | |
6 | 4, 1, 5 | co 7016 | . . 3 class (1 ·ℎ 𝐴) |
7 | 6, 1 | wceq 1522 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 28493 hvsubid 28494 hvaddsubval 28501 hv2times 28529 hvnegdii 28530 hilvc 28630 hhssnv 28732 h1de2bi 29022 h1datomi 29049 mayete3i 29196 homulid2 29268 lnop0 29434 lnopaddi 29439 lnophmlem2 29485 lnfn0i 29510 lnfnaddi 29511 strlem1 29718 |
Copyright terms: Public domain | W3C validator |