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 \in ℂ \land B \in ℂ) \to A B = B A$

Proof

Step	Hyp	Ref	Expression
1		dfcnqs	$⊢ ℂ = (𝑹 \times 𝑹) / E^{-1}$
2		mulcnsrec	$⊢ ((x \in 𝑹 \land y \in 𝑹) \land (z \in 𝑹 \land w \in 𝑹)) \to [⟨x, y⟩] E^{-1} [⟨z, w⟩] E^{-1} = [⟨(x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)), (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w)⟩] E^{-1}$
3		mulcnsrec	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (x \in 𝑹 \land y \in 𝑹)) \to [⟨z, w⟩] E^{-1} [⟨x, y⟩] E^{-1} = [⟨(z \cdot_{𝑹} x) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} y)), (w \cdot_{𝑹} x) +_{𝑹} (z \cdot_{𝑹} y)⟩] E^{-1}$
4		mulcomsr	$⊢ x \cdot_{𝑹} z = z \cdot_{𝑹} x$
5		mulcomsr	$⊢ y \cdot_{𝑹} w = w \cdot_{𝑹} y$
6	5	oveq2i	$⊢ {-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w) = {-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} y)$
7	4 6	oveq12i	$⊢ (x \cdot_{𝑹} z) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (y \cdot_{𝑹} w)) = (z \cdot_{𝑹} x) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} y))$
8		mulcomsr	$⊢ y \cdot_{𝑹} z = z \cdot_{𝑹} y$
9		mulcomsr	$⊢ x \cdot_{𝑹} w = w \cdot_{𝑹} x$
10	8 9	oveq12i	$⊢ (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) = (z \cdot_{𝑹} y) +_{𝑹} (w \cdot_{𝑹} x)$
11		addcomsr	$⊢ (z \cdot_{𝑹} y) +_{𝑹} (w \cdot_{𝑹} x) = (w \cdot_{𝑹} x) +_{𝑹} (z \cdot_{𝑹} y)$
12	10 11	eqtri	$⊢ (y \cdot_{𝑹} z) +_{𝑹} (x \cdot_{𝑹} w) = (w \cdot_{𝑹} x) +_{𝑹} (z \cdot_{𝑹} y)$
13	1 2 3 7 12	ecovcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$

Metamath Proof Explorer

Theorem axmulcom

Proof