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 29000 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2110 | . 2 wff 𝐴 ∈ ℋ |
4 | c1 10730 | . . . 4 class 1 | |
5 | csm 29002 | . . . 4 class ·ℎ | |
6 | 4, 1, 5 | co 7213 | . . 3 class (1 ·ℎ 𝐴) |
7 | 6, 1 | wceq 1543 | . 2 wff (1 ·ℎ 𝐴) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (1 ·ℎ 𝐴) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvmul0or 29106 hvsubid 29107 hvaddsubval 29114 hv2times 29142 hvnegdii 29143 hilvc 29243 hhssnv 29345 h1de2bi 29635 h1datomi 29662 mayete3i 29809 homulid2 29881 lnop0 30047 lnopaddi 30052 lnophmlem2 30098 lnfn0i 30123 lnfnaddi 30124 strlem1 30331 |
Copyright terms: Public domain | W3C validator |