Theorem axhvdistr1-zf

Description: Derive Axiom ax-hvdistr1 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}}$$
Assertion	axhvdistr1-zf	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\wedge C\in \mathscr{H}\right)\to A{\cdot }_{ℎ}\left(B{+}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){+}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
3		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	1	fveq2i	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
5	3 4	eqtr4i	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
6	2	hlnvi	$$⊢U\in \mathrm{NrmCVec}$$
7	1 6	h2hva	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
8	1 6	h2hsm	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
9	5 7 8	hldi	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge \left(A\in ℂ\wedge B\in \mathscr{H}\wedge C\in \mathscr{H}\right)\right)\to A{\cdot }_{ℎ}\left(B{+}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){+}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$
10	2 9	mpan	$$⊢\left(A\in ℂ\wedge B\in \mathscr{H}\wedge C\in \mathscr{H}\right)\to A{\cdot }_{ℎ}\left(B{+}_{ℎ}C\right)=\left(A{\cdot }_{ℎ}B\right){+}_{ℎ}\left(A{\cdot }_{ℎ}C\right)$$