Metamath Proof Explorer

Theorem cnncvsmulassdemo

Description: Derive the associative law for complex number multiplication mulass interpreted as scalar multiplication to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Assertion cnncvsmulassdemo ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ B ⁢ C

Proof

Step Hyp Ref Expression
1 eqid ⊢ ringLMod ⁡ ℂ fld = ringLMod ⁡ ℂ fld
2 1 cncvs ⊢ ringLMod ⁡ ℂ fld ∈ ℂVec
3 id ⊢ ringLMod ⁡ ℂ fld ∈ ℂVec → ringLMod ⁡ ℂ fld ∈ ℂVec
4 3 cvsclm ⊢ ringLMod ⁡ ℂ fld ∈ ℂVec → ringLMod ⁡ ℂ fld ∈ CMod
5 2 4 ax-mp ⊢ ringLMod ⁡ ℂ fld ∈ CMod
6 1 cnrbas ⊢ Base ringLMod ⁡ ℂ fld = ℂ
7 6 eqcomi ⊢ ℂ = Base ringLMod ⁡ ℂ fld
8 cnfldex ⊢ ℂ fld ∈ V
9 rlmsca ⊢ ℂ fld ∈ V → ℂ fld = Scalar ⁡ ringLMod ⁡ ℂ fld
10 8 9 ax-mp ⊢ ℂ fld = Scalar ⁡ ringLMod ⁡ ℂ fld
11 cnfldmul ⊢ × = ⋅ ℂ fld
12 rlmvsca ⊢ ⋅ ℂ fld = ⋅ ringLMod ⁡ ℂ fld
13 11 12 eqtri ⊢ × = ⋅ ringLMod ⁡ ℂ fld
14 cnfldbas ⊢ ℂ = Base ℂ fld
15 14 eqcomi ⊢ Base ℂ fld = ℂ
16 15 eqcomi ⊢ ℂ = Base ℂ fld
17 7 10 13 16 clmvsass ⊢ ringLMod ⁡ ℂ fld ∈ CMod ∧ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ B ⁢ C
18 5 17 mpan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ⁢ C = A ⁢ B ⁢ C