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