Theorem 2zrngmul

Description: The ring multiplication operation of R is the multiplication on complex numbers. (Contributed by AV, 31-Jan-2020)

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrngmul	⊢ · = ( .r ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		zex	⊢ ℤ ∈ V
4	1 3	rabex2	⊢ 𝐸 ∈ V
5	2	cnfldsrngmul	⊢ ( 𝐸 ∈ V → · = ( .r ‘ 𝑅 ) )
6	4 5	ax-mp	⊢ · = ( .r ‘ 𝑅 )