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	$$⊢\mathscr{H}\in \mathrm{V}$$
2		ax-hfvadd	$$⊢{+}_{ℎ}:\mathscr{H}\times \mathscr{H}⟶\mathscr{H}$$
3		ax-hvass	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\wedge z\in \mathscr{H}\right)\to \left(x{+}_{ℎ}y\right){+}_{ℎ}z=x{+}_{ℎ}\left(y{+}_{ℎ}z\right)$$
4		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
5		hvaddlid	$$⊢x\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}x=x$$
6		neg1cn	$$⊢-1\in ℂ$$
7		hvmulcl	$$⊢\left(-1\in ℂ\wedge x\in \mathscr{H}\right)\to -1{\cdot }_{ℎ}x\in \mathscr{H}$$
8	6 7	mpan	$$⊢x\in \mathscr{H}\to -1{\cdot }_{ℎ}x\in \mathscr{H}$$
9		ax-hvcom	$$⊢\left(-1{\cdot }_{ℎ}x\in \mathscr{H}\wedge x\in \mathscr{H}\right)\to \left(-1{\cdot }_{ℎ}x\right){+}_{ℎ}x=x{+}_{ℎ}\left(-1{\cdot }_{ℎ}x\right)$$
10	8 9	mpancom	$$⊢x\in \mathscr{H}\to \left(-1{\cdot }_{ℎ}x\right){+}_{ℎ}x=x{+}_{ℎ}\left(-1{\cdot }_{ℎ}x\right)$$
11		hvnegid	$$⊢x\in \mathscr{H}\to x{+}_{ℎ}\left(-1{\cdot }_{ℎ}x\right)=0_{ℎ}$$
12	10 11	eqtrd	$$⊢x\in \mathscr{H}\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}{+}_{ℎ}=\mathscr{H}\times \mathscr{H}$$
15		ax-hvcom	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{+}_{ℎ}y=y{+}_{ℎ}x$$
16	13 14 15	isabloi	$$⊢{+}_{ℎ}\in \mathrm{AbelOp}$$