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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )

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 ) ∈ ℂMod )
5	2 4	ax-mp	⊢ ( ringLMod ‘ ℂfld ) ∈ ℂMod
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	⊢ · = ( .r ‘ ℂfld )
12		rlmvsca	⊢ ( .r ‘ ℂ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 ) ∈ ℂMod ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )
18	5 17	mpan	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )