This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axmulcom

Description: Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom be used later. Instead, use mulcom . (Contributed by NM, 31-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion axmulcom 
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )

Proof

Step Hyp Ref Expression
1 dfcnqs 
 |-  CC = ( ( R. X. R. ) /. `' _E )
2 mulcnsrec 
 |-  ( ( ( x e. R. /\ y e. R. ) /\ ( z e. R. /\ w e. R. ) ) -> ( [ <. x , y >. ] `' _E x. [ <. z , w >. ] `' _E ) = [ <. ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) , ( ( y .R z ) +R ( x .R w ) ) >. ] `' _E )
3 mulcnsrec 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( x e. R. /\ y e. R. ) ) -> ( [ <. z , w >. ] `' _E x. [ <. x , y >. ] `' _E ) = [ <. ( ( z .R x ) +R ( -1R .R ( w .R y ) ) ) , ( ( w .R x ) +R ( z .R y ) ) >. ] `' _E )
4 mulcomsr 
 |-  ( x .R z ) = ( z .R x )
5 mulcomsr 
 |-  ( y .R w ) = ( w .R y )
6 5 oveq2i 
 |-  ( -1R .R ( y .R w ) ) = ( -1R .R ( w .R y ) )
7 4 6 oveq12i 
 |-  ( ( x .R z ) +R ( -1R .R ( y .R w ) ) ) = ( ( z .R x ) +R ( -1R .R ( w .R y ) ) )
8 mulcomsr 
 |-  ( y .R z ) = ( z .R y )
9 mulcomsr 
 |-  ( x .R w ) = ( w .R x )
10 8 9 oveq12i 
 |-  ( ( y .R z ) +R ( x .R w ) ) = ( ( z .R y ) +R ( w .R x ) )
11 addcomsr 
 |-  ( ( z .R y ) +R ( w .R x ) ) = ( ( w .R x ) +R ( z .R y ) )
12 10 11 eqtri 
 |-  ( ( y .R z ) +R ( x .R w ) ) = ( ( w .R x ) +R ( z .R y ) )
13 1 2 3 7 12 ecovcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )