![]() |
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 30801 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2098 | . 2 wff 𝐴 ∈ ℋ |
4 | c0v 30806 | . . . 4 class 0ℎ | |
5 | cva 30802 | . . . 4 class +ℎ | |
6 | 1, 4, 5 | co 7419 | . . 3 class (𝐴 +ℎ 0ℎ) |
7 | 6, 1 | wceq 1533 | . 2 wff (𝐴 +ℎ 0ℎ) = 𝐴 |
8 | 3, 7 | wi 4 | 1 wff (𝐴 ∈ ℋ → (𝐴 +ℎ 0ℎ) = 𝐴) |
Colors of variables: wff setvar class |
This axiom is referenced by: hvaddlid 30905 hvpncan 30921 hvsubeq0i 30945 hvsubcan2i 30946 hvsubaddi 30948 hvsub0 30958 hvaddsub4 30960 norm3difi 31029 shsel1 31203 shunssi 31250 omlsilem 31284 pjoc1i 31313 pjchi 31314 spansncvi 31534 5oalem1 31536 5oalem2 31537 3oalem2 31545 pjssmii 31563 hoaddridi 31668 lnop0 31848 lnopmul 31849 lnfn0i 31924 lnfnmuli 31926 pjclem4 32081 pj3si 32089 hst1h 32109 sumdmdlem 32300 |
Copyright terms: Public domain | W3C validator |