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 ) )