Metamath Proof Explorer

Theorem vcdir

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 vcdir ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B 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 ⊢ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → y + z S x = y S x G z S x
6 5 ralimi ⊢ ∀ z ∈ ℂ y + z S x = y S x G z S x ∧ y ⁢ z S x = y S z S x → ∀ z ∈ ℂ y + z S x = y S x G z S x
7 6 adantl ⊢ ∀ 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 ∈ ℂ y + z S x = y S x G z S x
8 7 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 ∈ ℂ y + z S x = y S x G z S x
9 8 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 ∈ ℂ y + z S x = y S x G z S x
10 9 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 ∈ ℂ y + z S x = y S x G z S x
11 10 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 ∈ ℂ y + z S x = y S x G z S x
12 4 11 syl ⊢ W ∈ CVec OLD → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ ℂ y + z S x = y S x G z S x
13 oveq2 ⊢ x = C → y + z S x = y + z S C
14 oveq2 ⊢ x = C → y S x = y S C
15 oveq2 ⊢ x = C → z S x = z S C
16 14 15 oveq12d ⊢ x = C → y S x G z S x = y S C G z S C
17 13 16 eqeq12d ⊢ x = C → y + z S x = y S x G z S x ↔ y + z S C = y S C G z S C
18 oveq1 ⊢ y = A → y + z = A + z
19 18 oveq1d ⊢ y = A → y + z S C = A + z S C
20 oveq1 ⊢ y = A → y S C = A S C
21 20 oveq1d ⊢ y = A → y S C G z S C = A S C G z S C
22 19 21 eqeq12d ⊢ y = A → y + z S C = y S C G z S C ↔ A + z S C = A S C G z S C
23 oveq2 ⊢ z = B → A + z = A + B
24 23 oveq1d ⊢ z = B → A + z S C = A + B S C
25 oveq1 ⊢ z = B → z S C = B S C
26 25 oveq2d ⊢ z = B → A S C G z S C = A S C G B S C
27 24 26 eqeq12d ⊢ z = B → A + z S C = A S C G z S C ↔ A + B S C = A S C G B S C
28 17 22 27 rspc3v ⊢ C ∈ X ∧ A ∈ ℂ ∧ B ∈ ℂ → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ ℂ y + z S x = y S x G z S x → A + B S C = A S C G B S C
29 12 28 syl5 ⊢ C ∈ X ∧ A ∈ ℂ ∧ B ∈ ℂ → W ∈ CVec OLD → A + B S C = A S C G B S C
30 29 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → W ∈ CVec OLD → A + B S C = A S C G B S C
31 30 impcom ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A + B S C = A S C G B S C