# Metamath Proof Explorer

## Theorem axhvcom-zf

Description: Derive axiom ax-hvcom from Hilbert space under ZF set theory. (Contributed by NM, 27-May-2008) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
axhil.2 ${⊢}{U}\in {CHil}_{\mathrm{OLD}}$
Assertion axhvcom-zf ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{+}_{ℎ}{B}={B}{+}_{ℎ}{A}$

### Proof

Step Hyp Ref Expression
1 axhil.1 ${⊢}{U}=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$
2 axhil.2 ${⊢}{U}\in {CHil}_{\mathrm{OLD}}$
3 df-hba ${⊢}ℋ=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
4 1 fveq2i ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$
5 3 4 eqtr4i ${⊢}ℋ=\mathrm{BaseSet}\left({U}\right)$
6 2 hlnvi ${⊢}{U}\in \mathrm{NrmCVec}$
7 1 6 h2hva ${⊢}{+}_{ℎ}={+}_{v}\left({U}\right)$
8 5 7 hlcom ${⊢}\left({U}\in {CHil}_{\mathrm{OLD}}\wedge {A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{+}_{ℎ}{B}={B}{+}_{ℎ}{A}$
9 2 8 mp3an1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{+}_{ℎ}{B}={B}{+}_{ℎ}{A}$