Theorem axhis4-zf

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

	Ref	Expression
Hypotheses	axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
	axhfi.1	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
Assertion	axhis4-zf	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$

Proof

Step	Hyp	Ref	Expression
1		axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
3		axhfi.1	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
4		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
5	1	fveq2i	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
6	4 5	eqtr4i	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
7		df-h0v	$$⊢0_{ℎ}=0_{\mathrm{vec}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
8	1	fveq2i	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
9	7 8	eqtr4i	$$⊢0_{ℎ}=0_{\mathrm{vec}}\left(U\right)$$
10	6 9 3	hlipgt0	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$
11	2 10	mp3an1	$$⊢\left(A\in \mathscr{H}\wedge A\ne 0_{ℎ}\right)\to 0<A{\cdot }_{\mathrm{ih}}A$$