Metamath Proof Explorer

Theorem vcass

Description: Associative 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 vcass ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S 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 simpr ⊢ 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 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 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 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 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 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 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 z S x
12 4 11 syl ⊢ W ∈ CVec OLD → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ ℂ y ⁢ z S x = y S z S x
13 oveq2 ⊢ x = C → y ⁢ z S x = y ⁢ z S C
14 oveq2 ⊢ x = C → z S x = z S C
15 14 oveq2d ⊢ x = C → y S z S x = y S z S C
16 13 15 eqeq12d ⊢ x = C → y ⁢ z S x = y S z S x ↔ y ⁢ z S C = y S z S C
17 oveq1 ⊢ y = A → y ⁢ z = A ⁢ z
18 17 oveq1d ⊢ y = A → y ⁢ z S C = A ⁢ z S C
19 oveq1 ⊢ y = A → y S z S C = A S z S C
20 18 19 eqeq12d ⊢ y = A → y ⁢ z S C = y S z S C ↔ A ⁢ z S C = A S z S C
21 oveq2 ⊢ z = B → A ⁢ z = A ⁢ B
22 21 oveq1d ⊢ z = B → A ⁢ z S C = A ⁢ B S C
23 oveq1 ⊢ z = B → z S C = B S C
24 23 oveq2d ⊢ z = B → A S z S C = A S B S C
25 22 24 eqeq12d ⊢ z = B → A ⁢ z S C = A S z S C ↔ A ⁢ B S C = A S B S C
26 16 20 25 rspc3v ⊢ C ∈ X ∧ A ∈ ℂ ∧ B ∈ ℂ → ∀ x ∈ X ∀ y ∈ ℂ ∀ z ∈ ℂ y ⁢ z S x = y S z S x → A ⁢ B S C = A S B S C
27 12 26 syl5 ⊢ C ∈ X ∧ A ∈ ℂ ∧ B ∈ ℂ → W ∈ CVec OLD → A ⁢ B S C = A S B S C
28 27 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → W ∈ CVec OLD → A ⁢ B S C = A S B S C
29 28 impcom ⊢ W ∈ CVec OLD ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ X → A ⁢ B S C = A S B S C