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 ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = 𝑹 × 𝑹 / E -1
2 mulcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x y E -1 ⁢ z w E -1 = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w E -1
3 mulcnsrec ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ x ∈ 𝑹 ∧ y ∈ 𝑹 → z w E -1 ⁢ x y E -1 = z ⋅ 𝑹 x + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 y w ⋅ 𝑹 x + 𝑹 z ⋅ 𝑹 y E -1
4 mulcomsr ⊢ x ⋅ 𝑹 z = z ⋅ 𝑹 x
5 mulcomsr ⊢ y ⋅ 𝑹 w = w ⋅ 𝑹 y
6 5 oveq2i ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w = -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 y
7 4 6 oveq12i ⊢ x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w = z ⋅ 𝑹 x + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 y
8 mulcomsr ⊢ y ⋅ 𝑹 z = z ⋅ 𝑹 y
9 mulcomsr ⊢ x ⋅ 𝑹 w = w ⋅ 𝑹 x
10 8 9 oveq12i ⊢ y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w = z ⋅ 𝑹 y + 𝑹 w ⋅ 𝑹 x
11 addcomsr ⊢ z ⋅ 𝑹 y + 𝑹 w ⋅ 𝑹 x = w ⋅ 𝑹 x + 𝑹 z ⋅ 𝑹 y
12 10 11 eqtri ⊢ y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w = w ⋅ 𝑹 x + 𝑹 z ⋅ 𝑹 y
13 1 2 3 7 12 ecovcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A