This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvdir

Description: Distributive law for the scalar product of a complex vector space. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvdi.1 ⊢ X = BaseSet ⁡ U
nvdi.2 ⊢ G = + v ⁡ U
nvdi.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
Assertion nvdir ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C

Proof

Step Hyp Ref Expression
1 nvdi.1 ⊢ X = BaseSet ⁡ U
2 nvdi.2 ⊢ G = + v ⁡ U
3 nvdi.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 eqid ⊢ 1 st ⁡ U = 1 st ⁡ U
5 4 nvvc ⊢ U ∈ NrmCVec → 1 st ⁡ U ∈ CVec OLD
6 2 vafval ⊢ G = 1 st ⁡ 1 st ⁡ U
7 3 smfval ⊢ S = 2 nd ⁡ 1 st ⁡ U
8 1 2 bafval ⊢ X = ran ⁡ G
9 6 7 8 vcdir ⊢ 1 st ⁡ U ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C
10 5 9 sylan ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C