![]() |
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 28352 | . . 3 class ℋ | |
3 | 1, 2 | wcel 2107 | . 2 wff 𝐴 ∈ ℋ |
4 | c0v 28357 | . . . 4 class 0ℎ | |
5 | cva 28353 | . . . 4 class +ℎ | |
6 | 1, 4, 5 | co 6924 | . . 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 28456 hvpncan 28472 hvsubeq0i 28496 hvsubcan2i 28497 hvsubaddi 28499 hvsub0 28509 hvaddsub4 28511 norm3difi 28580 shsel1 28756 shunssi 28803 omlsilem 28837 pjoc1i 28866 pjchi 28867 spansncvi 29087 5oalem1 29089 5oalem2 29090 3oalem2 29098 pjssmii 29116 hoaddid1i 29221 lnop0 29401 lnopmul 29402 lnfn0i 29477 lnfnmuli 29479 pjclem4 29634 pj3si 29642 hst1h 29662 sumdmdlem 29853 |
Copyright terms: Public domain | W3C validator |