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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = ( ( R × R ) / ◡ E )
2 mulcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E · [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) , ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ⟩ ] ◡ E )
3 mulcnsrec ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E · [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑧 ·R 𝑥 ) +R ( -1R ·R ( 𝑤 ·R 𝑦 ) ) ) , ( ( 𝑤 ·R 𝑥 ) +R ( 𝑧 ·R 𝑦 ) ) ⟩ ] ◡ E )
4 mulcomsr ⊢ ( 𝑥 ·R 𝑧 ) = ( 𝑧 ·R 𝑥 )
5 mulcomsr ⊢ ( 𝑦 ·R 𝑤 ) = ( 𝑤 ·R 𝑦 )
6 5 oveq2i ⊢ ( -1R ·R ( 𝑦 ·R 𝑤 ) ) = ( -1R ·R ( 𝑤 ·R 𝑦 ) )
7 4 6 oveq12i ⊢ ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) = ( ( 𝑧 ·R 𝑥 ) +R ( -1R ·R ( 𝑤 ·R 𝑦 ) ) )
8 mulcomsr ⊢ ( 𝑦 ·R 𝑧 ) = ( 𝑧 ·R 𝑦 )
9 mulcomsr ⊢ ( 𝑥 ·R 𝑤 ) = ( 𝑤 ·R 𝑥 )
10 8 9 oveq12i ⊢ ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) = ( ( 𝑧 ·R 𝑦 ) +R ( 𝑤 ·R 𝑥 ) )
11 addcomsr ⊢ ( ( 𝑧 ·R 𝑦 ) +R ( 𝑤 ·R 𝑥 ) ) = ( ( 𝑤 ·R 𝑥 ) +R ( 𝑧 ·R 𝑦 ) )
12 10 11 eqtri ⊢ ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) = ( ( 𝑤 ·R 𝑥 ) +R ( 𝑧 ·R 𝑦 ) )
13 1 2 3 7 12 ecovcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )