Theorem dfcnfldOLD

Description: Obsolete version of df-cnfld as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Thierry Arnoux, 15-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dfcnfldOLD	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-cnfld	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\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)⟩\right\}\right)$$
2		eqidd	$$⊢\top \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩$$
3		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
4		ffn	$$⊢+:ℂ\times ℂ⟶ℂ\to +Fn\left(ℂ\times ℂ\right)$$
5	3 4	ax-mp	$$⊢+Fn\left(ℂ\times ℂ\right)$$
6		fnov	$$⊢+Fn\left(ℂ\times ℂ\right)\leftrightarrow +=\left(u\in ℂ,v\in ℂ⟼u+v\right)$$
7	5 6	mpbi	$$⊢+=\left(u\in ℂ,v\in ℂ⟼u+v\right)$$
8		eqcom	$$⊢+=\left(u\in ℂ,v\in ℂ⟼u+v\right)\leftrightarrow \left(u\in ℂ,v\in ℂ⟼u+v\right)=+$$
9	7 8	mpbi	$$⊢\left(u\in ℂ,v\in ℂ⟼u+v\right)=+$$
10	9	opeq2i	$$⊢⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩=⟨{+}_{\mathrm{ndx}},+⟩$$
11	10	a1i	$$⊢\top \to ⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩=⟨{+}_{\mathrm{ndx}},+⟩$$
12		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
13		ffn	$$⊢\times :ℂ\times ℂ⟶ℂ\to \times Fn\left(ℂ\times ℂ\right)$$
14	12 13	ax-mp	$$⊢\times Fn\left(ℂ\times ℂ\right)$$
15		fnov	$$⊢\times Fn\left(ℂ\times ℂ\right)\leftrightarrow \times =\left(u\in ℂ,v\in ℂ⟼uv\right)$$
16	14 15	mpbi	$$⊢\times =\left(u\in ℂ,v\in ℂ⟼uv\right)$$
17		eqcom	$$⊢\times =\left(u\in ℂ,v\in ℂ⟼uv\right)\leftrightarrow \left(u\in ℂ,v\in ℂ⟼uv\right)=\times$$
18	16 17	mpbi	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)=\times$$
19	18	opeq2i	$$⊢⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\times ⟩$$
20	19	a1i	$$⊢\top \to ⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩=⟨{\cdot }_{\mathrm{ndx}},\times ⟩$$
21	2 11 20	tpeq123d	$$⊢\top \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
22	21	mptru	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
23	22	uneq1i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\right)⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}\cup \left\{⟨{\mathrm{*}}_{\mathrm{ndx}},*⟩\right\}$$
24	23	uneq1i	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼u+v\right)⟩,⟨{\cdot }_{\mathrm{ndx}},\left(u\in ℂ,v\in ℂ⟼uv\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)⟩\right\}\right)=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)$$
25	1 24	eqtri	$$⊢{ℂ}_{\mathrm{fld}}=\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\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)⟩\right\}\right)$$