Theorem fldedom

Description: A field is a Euclidean domain, regardless of its Euclidean norm. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Hypotheses	fldedom.b	$$⊢B={\mathrm{Base}}_F$$
	fldedom.1	$$⊢\underset{\dot{}}{0}=0_F$$
	fldedom.2	$$⊢W=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
	fldedom.e	$$⊢E=\mathrm{EuclF}\left(F\right)$$
	fldedom.f	$$⊢\phi \to F\in \mathrm{Field}$$
	fldedom.3	$$⊢\phi \to \left({E\upharpoonright }_W\right):W⟶{\mathbb{N}}_0$$
Assertion	fldedom	$$⊢\phi \to F\in \mathrm{EDomn}$$

Proof

Step	Hyp	Ref	Expression
1		fldedom.b	$$⊢B={\mathrm{Base}}_F$$
2		fldedom.1	$$⊢\underset{\dot{}}{0}=0_F$$
3		fldedom.2	$$⊢W=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
4		fldedom.e	$$⊢E=\mathrm{EuclF}\left(F\right)$$
5		fldedom.f	$$⊢\phi \to F\in \mathrm{Field}$$
6		fldedom.3	$$⊢\phi \to \left({E\upharpoonright }_W\right):W⟶{\mathbb{N}}_0$$
7		fldidom	$$⊢F\in \mathrm{Field}\to F\in \mathrm{IDomn}$$
8	5 7	syl	$$⊢\phi \to F\in \mathrm{IDomn}$$
9	3	reseq2i	$$⊢{E\upharpoonright }_W={E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}$$
10	9	a1i	$$⊢\phi \to {E\upharpoonright }_W={E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}$$
11	3	a1i	$$⊢\phi \to W=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
12	11 6	feq2dd	$$⊢\phi \to \left({E\upharpoonright }_W\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0$$
13	10 12	feq1dd	$$⊢\phi \to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0$$
14		oveq2	$$⊢q={inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\to y{\cdot }_{F}q=y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)$$
15	14	oveq1d	$$⊢q={inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\to \left(y{\cdot }_{F}q\right){+}_{F}r=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r$$
16	15	eqeq2d	$$⊢q={inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\to \left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\leftrightarrow x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r\right)$$
17	16	anbi1d	$$⊢q={inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\to \left(\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \left(x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)$$
18		oveq2	$$⊢r=\underset{\dot{}}{0}\to \left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}$$
19	18	eqeq2d	$$⊢r=\underset{\dot{}}{0}\to \left(x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r\leftrightarrow x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}\right)$$
20		eqeq1	$$⊢r=\underset{\dot{}}{0}\to \left(r=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
21		fveq2	$$⊢r=\underset{\dot{}}{0}\to \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)=\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)$$
22	21	breq1d	$$⊢r=\underset{\dot{}}{0}\to \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\leftrightarrow \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)$$
23	20 22	orbi12d	$$⊢r=\underset{\dot{}}{0}\to \left(\left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\leftrightarrow \left(\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
24	19 23	anbi12d	$$⊢r=\underset{\dot{}}{0}\to \left(\left(x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\leftrightarrow \left(x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}\wedge \left(\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)$$
25		eqid	$$⊢{\cdot }_F={\cdot }_F$$
26	8	idomringd	$$⊢\phi \to F\in \mathrm{Ring}$$
27	26	ad2antrr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to F\in \mathrm{Ring}$$
28		eqid	$$⊢{inv}_r\left(F\right)={inv}_r\left(F\right)$$
29	5	flddrngd	$$⊢\phi \to F\in \mathrm{DivRing}$$
30	29	ad2antrr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to F\in \mathrm{DivRing}$$
31		difssd	$$⊢\left(\phi \wedge x\in B\right)\to B\setminus \left\{\underset{\dot{}}{0}\right\}\subseteq B$$
32	31	sselda	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y\in B$$
33		simpr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
34	33	eldifsnbd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y\ne \underset{\dot{}}{0}$$
35	1 2 28 30 32 34	drnginvrcld	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to {inv}_r\left(F\right)\left(y\right)\in B$$
36		simplr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x\in B$$
37	1 25 27 35 36	ringcld	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to {inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\in B$$
38	26	ringgrpd	$$⊢\phi \to F\in \mathrm{Grp}$$
39	1 2 38	grpidcld	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
40	39	ad2antrr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \underset{\dot{}}{0}\in B$$
41		eqid	$$⊢{+}_F={+}_F$$
42	38	ad2antrr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to F\in \mathrm{Grp}$$
43	1 25 27 32 37	ringcld	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\in B$$
44	1 41 2 42 43	grpridd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}=y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)$$
45	1 25 27 32 35 36	ringassd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(y{\cdot }_F{inv}_r\left(F\right)\left(y\right)\right){\cdot }_{F}x=y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)$$
46		eqid	$$⊢1_F=1_F$$
47	1 2 25 46 28 30 32 34	drnginvrrd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y{\cdot }_F{inv}_r\left(F\right)\left(y\right)=1_F$$
48	47	oveq1d	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(y{\cdot }_F{inv}_r\left(F\right)\left(y\right)\right){\cdot }_{F}x=1_F{\cdot }_{F}x$$
49	45 48	eqtr3d	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)=1_F{\cdot }_{F}x$$
50	1 25 46 27 36	ringlidmd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to 1_F{\cdot }_{F}x=x$$
51	44 49 50	3eqtrrd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}$$
52		eqidd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{0}$$
53	52	orcd	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)$$
54	51 53	jca	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(x=\left(y{\cdot }_F\left({inv}_r\left(F\right)\left(y\right){\cdot }_{F}x\right)\right){+}_F\underset{\dot{}}{0}\wedge \left(\underset{\dot{}}{0}=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(\underset{\dot{}}{0}\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
55	17 24 37 40 54	2rspcedvdw	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \exists q\in B\exists r\in B\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
56	55	anasss	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\to \exists q\in B\exists r\in B\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
57	56	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)$$
58	13 57	jca	$$⊢\phi \to \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0\wedge \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)$$
59	4	reseq1i	$$⊢{E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}={\mathrm{EuclF}\left(F\right)\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}$$
60	1 2 41 25 59	isedom	$$⊢F\in \mathrm{EDomn}\leftrightarrow \left(F\in \mathrm{IDomn}\wedge \left(\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right):B\setminus \left\{\underset{\dot{}}{0}\right\}⟶{\mathbb{N}}_0\wedge \forall x\in B\forall y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\exists q\in B\exists r\in B\left(x=\left(y{\cdot }_{F}q\right){+}_{F}r\wedge \left(r=\underset{\dot{}}{0}\vee \left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(r\right)<\left({E\upharpoonright }_{\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)}\right)\left(y\right)\right)\right)\right)\right)$$
61	8 58 60	sylanbrc	$$⊢\phi \to F\in \mathrm{EDomn}$$