hhba

Description: The base set of Hilbert space. This theorem provides an independent proof of df-hba (see comments in that definition). (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	Assertion	hhba	$⊢ ℋ = BaseSet (U)$

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		hilablo	$⊢ +_{ℎ} \in AbelOp$
3		ablogrpo	$⊢ +_{ℎ} \in AbelOp \to +_{ℎ} \in GrpOp$
4	2 3	ax-mp	$⊢ +_{ℎ} \in GrpOp$
5		ax-hfvadd	$⊢ +_{ℎ} : ℋ \times ℋ ⟶ ℋ$
6	5	fdmi	$⊢ dom +_{ℎ} = ℋ \times ℋ$
7	4 6	grporn	$⊢ ℋ = ran +_{ℎ}$
8		eqid	$⊢ BaseSet (U) = BaseSet (U)$
9	1	hhva	$⊢ +_{ℎ} = +_{v} (U)$
10	8 9	bafval	$⊢ BaseSet (U) = ran +_{ℎ}$
11	7 10	eqtr4i	$⊢ ℋ = BaseSet (U)$

Metamath Proof Explorer

Theorem hhba

Proof