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 | chil 27160 | . . 3 class ℋ | |
3 | 1, 2 | wcel 1977 | . 2 wff 𝐴 ∈ ℋ |
4 | c0v 27165 | . . . 4 class 0ℎ | |
5 | cva 27161 | . . . 4 class +ℎ | |
6 | 1, 4, 5 | co 6549 | . . 3 class (𝐴 +ℎ 0ℎ) |
7 | 6, 1 | wceq 1475 | . 2 wff (𝐴 +ℎ 0ℎ) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvaddid2 27264 hvpncan 27280 hvsubeq0i 27304 hvsubcan2i 27305 hvsubaddi 27307 hvsub0 27317 hvaddsub4 27319 norm3difi 27388 shsel1 27564 shunssi 27611 omlsilem 27645 pjoc1i 27674 pjchi 27675 spansncvi 27895 5oalem1 27897 5oalem2 27898 3oalem2 27906 pjssmii 27924 hoaddid1i 28029 lnop0 28209 lnopmul 28210 lnfn0i 28285 lnfnmuli 28287 pjclem4 28442 pj3si 28450 hst1h 28470 sumdmdlem 28661 |
Copyright terms: Public domain | W3C validator |