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	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zrngbas.r	|- R = ( CCfld |`s E )
Assertion	2zrngmul	|- x. = ( .r ` R )

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2		2zrngbas.r	|- R = ( CCfld |`s E )
3		zex	|- ZZ e. _V
4	1 3	rabex2	|- E e. _V
5	2	cnfldsrngmul	|- ( E e. _V -> x. = ( .r ` R ) )
6	4 5	ax-mp	|- x. = ( .r ` R )