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		hvaddid2	⊢ ( 𝑥 ∈ ℋ → ( 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