Theorem mpocnfldmul

Description: The multiplication operation of the field of complex numbers. Version of cnfldmul using maps-to notation, which does not require ax-mulf . (Contributed by GG, 31-Mar-2025) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Assertion	mpocnfldmul	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)={\cdot }_{{ℂ}_{\mathrm{fld}}}$$

Proof

Step	Hyp	Ref	Expression
1		mpomulex	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)\in \mathrm{V}$$
2		cnfldstr	$$⊢{ℂ}_{\mathrm{fld}}\mathrm{Struct}⟨1,21⟩$$
3		mulridx	$$⊢{\cdot }_{𝑟}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
4		snsstp3	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}$$
5		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
6		ssun1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
7		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\right)\cup \left(\left\{⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),\mathrm{MetOpen}\left(\mathrm{abs}\circ -\right)⟩,⟨{\le }_{\mathrm{ndx}},\le ⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\mathrm{abs}\circ -⟩\right\}\cup \left\{⟨\mathrm{UnifSet}\left(\mathrm{ndx}\right),\mathrm{metUnif}\left(\mathrm{abs}\circ -\right)⟩,⟨\mathrm{EuclF}\left(\mathrm{ndx}\right),\mathrm{abs}⟩\right\}\right)$$
8	6 7	sseqtrri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
9	5 8	sstri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼x+y\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
10	4 9	sstri	$$⊢\left\{⟨{\cdot }_{\mathrm{ndx}},\left(x\in ℂ,y\in ℂ⟼xy\right)⟩\right\}\subseteq {ℂ}_{\mathrm{fld}}$$
11	2 3 10	strfv	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)\in \mathrm{V}\to \left(x\in ℂ,y\in ℂ⟼xy\right)={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
12	1 11	ax-mp	$$⊢\left(x\in ℂ,y\in ℂ⟼xy\right)={\cdot }_{{ℂ}_{\mathrm{fld}}}$$