# Metamath Proof Explorer

## Theorem hilablo

Description: Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hilablo ${⊢}{+}_{ℎ}\in \mathrm{AbelOp}$

### Proof

Step Hyp Ref Expression
1 ax-hilex ${⊢}ℋ\in \mathrm{V}$
2 ax-hfvadd ${⊢}{+}_{ℎ}:ℋ×ℋ⟶ℋ$
3 ax-hvass ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\wedge {z}\in ℋ\right)\to \left({x}{+}_{ℎ}{y}\right){+}_{ℎ}{z}={x}{+}_{ℎ}\left({y}{+}_{ℎ}{z}\right)$
4 ax-hv0cl ${⊢}{0}_{ℎ}\in ℋ$
5 hvaddid2 ${⊢}{x}\in ℋ\to {0}_{ℎ}{+}_{ℎ}{x}={x}$
6 neg1cn ${⊢}-1\in ℂ$
7 hvmulcl ${⊢}\left(-1\in ℂ\wedge {x}\in ℋ\right)\to -1{\cdot }_{ℎ}{x}\in ℋ$
8 6 7 mpan ${⊢}{x}\in ℋ\to -1{\cdot }_{ℎ}{x}\in ℋ$
9 ax-hvcom ${⊢}\left(-1{\cdot }_{ℎ}{x}\in ℋ\wedge {x}\in ℋ\right)\to \left(-1{\cdot }_{ℎ}{x}\right){+}_{ℎ}{x}={x}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{x}\right)$
10 8 9 mpancom ${⊢}{x}\in ℋ\to \left(-1{\cdot }_{ℎ}{x}\right){+}_{ℎ}{x}={x}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{x}\right)$
11 hvnegid ${⊢}{x}\in ℋ\to {x}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{x}\right)={0}_{ℎ}$
12 10 11 eqtrd ${⊢}{x}\in ℋ\to \left(-1{\cdot }_{ℎ}{x}\right){+}_{ℎ}{x}={0}_{ℎ}$
13 1 2 3 4 5 8 12 isgrpoi ${⊢}{+}_{ℎ}\in \mathrm{GrpOp}$
14 2 fdmi ${⊢}\mathrm{dom}{+}_{ℎ}=ℋ×ℋ$
15 ax-hvcom ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\right)\to {x}{+}_{ℎ}{y}={y}{+}_{ℎ}{x}$
16 13 14 15 isabloi ${⊢}{+}_{ℎ}\in \mathrm{AbelOp}$