This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ + ℎ ∈ AbelOp

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 ax-hfvadd ⊢ + ℎ : ℋ × ℋ ⟶ ℋ
3 ax-hvass ⊢ x ∈ ℋ ∧ y ∈ ℋ ∧ z ∈ ℋ → x + ℎ y + ℎ z = x + ℎ y + ℎ z
4 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
5 hvaddlid ⊢ x ∈ ℋ → 0 ℎ + ℎ x = x
6 neg1cn ⊢ − 1 ∈ ℂ
7 hvmulcl ⊢ − 1 ∈ ℂ ∧ x ∈ ℋ → -1 ⋅ ℎ x ∈ ℋ
8 6 7 mpan ⊢ x ∈ ℋ → -1 ⋅ ℎ x ∈ ℋ
9 ax-hvcom ⊢ -1 ⋅ ℎ x ∈ ℋ ∧ x ∈ ℋ → -1 ⋅ ℎ x + ℎ x = x + ℎ -1 ⋅ ℎ x
10 8 9 mpancom ⊢ x ∈ ℋ → -1 ⋅ ℎ x + ℎ x = x + ℎ -1 ⋅ ℎ x
11 hvnegid ⊢ x ∈ ℋ → x + ℎ -1 ⋅ ℎ x = 0 ℎ
12 10 11 eqtrd ⊢ x ∈ ℋ → -1 ⋅ ℎ x + ℎ x = 0 ℎ
13 1 2 3 4 5 8 12 isgrpoi ⊢ + ℎ ∈ GrpOp
14 2 fdmi ⊢ dom ⁡ + ℎ = ℋ × ℋ
15 ax-hvcom ⊢ x ∈ ℋ ∧ y ∈ ℋ → x + ℎ y = y + ℎ x
16 13 14 15 isabloi ⊢ + ℎ ∈ AbelOp