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 ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ) → ( ( 𝑥 +ℎ 𝑦 ) +ℎ 𝑧 ) = ( 𝑥 +ℎ ( 𝑦 +ℎ 𝑧 ) ) )
4 ax-hv0cl ⊢ 0ℎ ∈ ℋ
5 hvaddlid ⊢ ( 𝑥 ∈ ℋ → ( 0ℎ +ℎ 𝑥 ) = 𝑥 )
6 neg1cn ⊢ - 1 ∈ ℂ
7 hvmulcl ⊢ ( ( - 1 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( - 1 ·ℎ 𝑥 ) ∈ ℋ )
8 6 7 mpan ⊢ ( 𝑥 ∈ ℋ → ( - 1 ·ℎ 𝑥 ) ∈ ℋ )
9 ax-hvcom ⊢ ( ( ( - 1 ·ℎ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( - 1 ·ℎ 𝑥 ) +ℎ 𝑥 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑥 ) ) )
10 8 9 mpancom ⊢ ( 𝑥 ∈ ℋ → ( ( - 1 ·ℎ 𝑥 ) +ℎ 𝑥 ) = ( 𝑥 +ℎ ( - 1 ·ℎ 𝑥 ) ) )
11 hvnegid ⊢ ( 𝑥 ∈ ℋ → ( 𝑥 +ℎ ( - 1 ·ℎ 𝑥 ) ) = 0ℎ )
12 10 11 eqtrd ⊢ ( 𝑥 ∈ ℋ → ( ( - 1 ·ℎ 𝑥 ) +ℎ 𝑥 ) = 0ℎ )
13 1 2 3 4 5 8 12 isgrpoi ⊢ +ℎ ∈ GrpOp
14 2 fdmi ⊢ dom +ℎ = ( ℋ × ℋ )
15 ax-hvcom ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) = ( 𝑦 +ℎ 𝑥 ) )
16 13 14 15 isabloi ⊢ +ℎ ∈ AbelOp