![]() |
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 28348 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2107 | . 2 wff 𝐴 ∈ ℋ |
4 | c0v 28353 | . . . 4 class 0ℎ | |
5 | cva 28349 | . . . 4 class +ℎ | |
6 | 1, 4, 5 | co 6922 | . . 3 class (𝐴 +ℎ 0ℎ) |
7 | 6, 1 | wceq 1601 | . 2 wff (𝐴 +ℎ 0ℎ) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvaddid2 28452 hvpncan 28468 hvsubeq0i 28492 hvsubcan2i 28493 hvsubaddi 28495 hvsub0 28505 hvaddsub4 28507 norm3difi 28576 shsel1 28752 shunssi 28799 omlsilem 28833 pjoc1i 28862 pjchi 28863 spansncvi 29083 5oalem1 29085 5oalem2 29086 3oalem2 29094 pjssmii 29112 hoaddid1i 29217 lnop0 29397 lnopmul 29398 lnfn0i 29473 lnfnmuli 29475 pjclem4 29630 pj3si 29638 hst1h 29658 sumdmdlem 29849 |
Copyright terms: Public domain | W3C validator |