Metamath Proof Explorer

Theorem vcdi

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

Ref Expression
Hypotheses vciOLD.1 ⊢ G = 1 st ⁡ W
vciOLD.2 ⊢ S = 2 nd ⁡ W
vciOLD.3 ⊢ X = ran ⁡ G
Assertion vcdi ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B G C = A S B G A S C

Proof

Step Hyp Ref Expression
1 vciOLD.1 ⊢ G = 1 st ⁡ W
2 vciOLD.2 ⊢ S = 2 nd ⁡ W
3 vciOLD.3 ⊢ X = ran ⁡ G
4 1 2 3 vciOLD ⊢ W ∈ CVec OLD → G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x
5 simpl ⊢ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ z ∈ X y S x G z = y S x G y S z
6 5 ralimi ⊢ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z
7 6 adantl ⊢ 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z
8 7 ralimi ⊢ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z
9 8 3ad2ant3 ⊢ G ∈ AbelOp ∧ S : ℂ × X ⟶ X ∧ ∀ x ∈ X 1 S x = x ∧ ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z ∧ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z
10 4 9 syl ⊢ W ∈ CVec OLD → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z
11 oveq1 ⊢ x = B → x G z = B G z
12 11 oveq2d ⊢ x = B → y S x G z = y S B G z
13 oveq2 ⊢ x = B → y S x = y S B
14 13 oveq1d ⊢ x = B → y S x G y S z = y S B G y S z
15 12 14 eqeq12d ⊢ x = B → y S x G z = y S x G y S z ↔ y S B G z = y S B G y S z
16 oveq1 ⊢ y = A → y S B G z = A S B G z
17 oveq1 ⊢ y = A → y S B = A S B
18 oveq1 ⊢ y = A → y S z = A S z
19 17 18 oveq12d ⊢ y = A → y S B G y S z = A S B G A S z
20 16 19 eqeq12d ⊢ y = A → y S B G z = y S B G y S z ↔ A S B G z = A S B G A S z
21 oveq2 ⊢ z = C → B G z = B G C
22 21 oveq2d ⊢ z = C → A S B G z = A S B G C
23 oveq2 ⊢ z = C → A S z = A S C
24 23 oveq2d ⊢ z = C → A S B G A S z = A S B G A S C
25 22 24 eqeq12d ⊢ z = C → A S B G z = A S B G A S z ↔ A S B G C = A S B G A S C
26 15 20 25 rspc3v ⊢ B ∈ X ∧ A ∈ ℂ ∧ C ∈ X → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ X y S x G z = y S x G y S z → A S B G C = A S B G A S C
27 10 26 syl5 ⊢ B ∈ X ∧ A ∈ ℂ ∧ C ∈ X → W ∈ CVec OLD → A S B G C = A S B G A S C
28 27 3com12 ⊢ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → W ∈ CVec OLD → A S B G C = A S B G A S C
29 28 impcom ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ X ∧ C ∈ X → A S B G C = A S B G A S C