| Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > HSE Home > Th. List > ax-hvaddid | Structured version Visualization version GIF version | ||
| Description: Addition with the zero vector. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| ax-hvaddid | ⊢ (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | chba 30938 | . . 3 class ℋ | |
| 3 | 1, 2 | wcel 2108 | . 2 wff 𝐴 ∈ ℋ |
| 4 | c0v 30943 | . . . 4 class 0ℎ | |
| 5 | cva 30939 | . . . 4 class +ℎ | |
| 6 | 1, 4, 5 | co 7431 | . . 3 class (𝐴 +ℎ 0ℎ) |
| 7 | 6, 1 | wceq 1540 | . 2 wff (𝐴 +ℎ 0ℎ) = 𝐴 |
| 8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) |
| Colors of variables: wff setvar class |
| This axiom is referenced by: hvaddlid 31042 hvpncan 31058 hvsubeq0i 31082 hvsubcan2i 31083 hvsubaddi 31085 hvsub0 31095 hvaddsub4 31097 norm3difi 31166 shsel1 31340 shunssi 31387 omlsilem 31421 pjoc1i 31450 pjchi 31451 spansncvi 31671 5oalem1 31673 5oalem2 31674 3oalem2 31682 pjssmii 31700 hoaddridi 31805 lnop0 31985 lnopmul 31986 lnfn0i 32061 lnfnmuli 32063 pjclem4 32218 pj3si 32226 hst1h 32246 sumdmdlem 32437 |
| Copyright terms: Public domain | W3C validator |