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 e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ringLMod ` CCfld ) = ( ringLMod ` CCfld )
2 1 cncvs 
 |-  ( ringLMod ` CCfld ) e. CVec
3 id 
 |-  ( ( ringLMod ` CCfld ) e. CVec -> ( ringLMod ` CCfld ) e. CVec )
4 3 cvsclm 
 |-  ( ( ringLMod ` CCfld ) e. CVec -> ( ringLMod ` CCfld ) e. CMod )
5 2 4 ax-mp 
 |-  ( ringLMod ` CCfld ) e. CMod
6 1 cnrbas 
 |-  ( Base ` ( ringLMod ` CCfld ) ) = CC
7 6 eqcomi 
 |-  CC = ( Base ` ( ringLMod ` CCfld ) )
8 cnfldex 
 |-  CCfld e. _V
9 rlmsca 
 |-  ( CCfld e. _V -> CCfld = ( Scalar ` ( ringLMod ` CCfld ) ) )
10 8 9 ax-mp 
 |-  CCfld = ( Scalar ` ( ringLMod ` CCfld ) )
11 cnfldmul 
 |-  x. = ( .r ` CCfld )
12 rlmvsca 
 |-  ( .r ` CCfld ) = ( .s ` ( ringLMod ` CCfld ) )
13 11 12 eqtri 
 |-  x. = ( .s ` ( ringLMod ` CCfld ) )
14 cnfldbas 
 |-  CC = ( Base ` CCfld )
15 14 eqcomi 
 |-  ( Base ` CCfld ) = CC
16 15 eqcomi 
 |-  CC = ( Base ` CCfld )
17 7 10 13 16 clmvsass 
 |-  ( ( ( ringLMod ` CCfld ) e. CMod /\ ( A e. CC /\ B e. CC /\ C e. CC ) ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
18 5 17 mpan 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )