Metamath Proof Explorer


Axiom ax-mulass

Description: Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by Theorem axmulass . Proofs should normally use mulass instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-mulass ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA โŠข ๐ด
1 cc โŠข โ„‚
2 0 1 wcel โŠข ๐ด โˆˆ โ„‚
3 cB โŠข ๐ต
4 3 1 wcel โŠข ๐ต โˆˆ โ„‚
5 cC โŠข ๐ถ
6 5 1 wcel โŠข ๐ถ โˆˆ โ„‚
7 2 4 6 w3a โŠข ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ )
8 cmul โŠข ยท
9 0 3 8 co โŠข ( ๐ด ยท ๐ต )
10 9 5 8 co โŠข ( ( ๐ด ยท ๐ต ) ยท ๐ถ )
11 3 5 8 co โŠข ( ๐ต ยท ๐ถ )
12 0 11 8 co โŠข ( ๐ด ยท ( ๐ต ยท ๐ถ ) )
13 10 12 wceq โŠข ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) )
14 7 13 wi โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„‚ ) โ†’ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) = ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) )