Metamath Proof Explorer

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 ⊢ 𝐵 = ( Base ‘ 𝐹 )
fldedom.1 ⊢ 0 = ( 0g ‘ 𝐹 )
fldedom.2 ⊢ 𝑊 = ( 𝐵 ∖ { 0 } )
fldedom.e ⊢ 𝐸 = ( EuclF ‘ 𝐹 )
fldedom.f ⊢ ( 𝜑 → 𝐹 ∈ Field )
fldedom.3 ⊢ ( 𝜑 → ( 𝐸 ↾ 𝑊 ) : 𝑊 ⟶ ℕ0 )
Assertion fldedom ( 𝜑 → 𝐹 ∈ EDomn )

Proof

Step Hyp Ref Expression
1 fldedom.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
2 fldedom.1 ⊢ 0 = ( 0g ‘ 𝐹 )
3 fldedom.2 ⊢ 𝑊 = ( 𝐵 ∖ { 0 } )
4 fldedom.e ⊢ 𝐸 = ( EuclF ‘ 𝐹 )
5 fldedom.f ⊢ ( 𝜑 → 𝐹 ∈ Field )
6 fldedom.3 ⊢ ( 𝜑 → ( 𝐸 ↾ 𝑊 ) : 𝑊 ⟶ ℕ0 )
7 fldidom ⊢ ( 𝐹 ∈ Field → 𝐹 ∈ IDomn )
8 5 7 syl ⊢ ( 𝜑 → 𝐹 ∈ IDomn )
9 3 reseq2i ⊢ ( 𝐸 ↾ 𝑊 ) = ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) )
10 9 a1i ⊢ ( 𝜑 → ( 𝐸 ↾ 𝑊 ) = ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) )
11 3 a1i ⊢ ( 𝜑 → 𝑊 = ( 𝐵 ∖ { 0 } ) )
12 11 6 feq2dd ⊢ ( 𝜑 → ( 𝐸 ↾ 𝑊 ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 )
13 10 12 feq1dd ⊢ ( 𝜑 → ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 )
14 oveq2 ⊢ ( 𝑞 = ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) → ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) = ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) )
15 14 oveq1d ⊢ ( 𝑞 = ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) → ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) )
16 15 eqeq2d ⊢ ( 𝑞 = ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) → ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ↔ 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) ) )
17 16 anbi1d ⊢ ( 𝑞 = ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) → ( ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) )
18 oveq2 ⊢ ( 𝑟 = 0 → ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) )
19 18 eqeq2d ⊢ ( 𝑟 = 0 → ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) ↔ 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) ) )
20 eqeq1 ⊢ ( 𝑟 = 0 → ( 𝑟 = 0 ↔ 0 = 0 ) )
21 fveq2 ⊢ ( 𝑟 = 0 → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) = ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) )
22 21 breq1d ⊢ ( 𝑟 = 0 → ( ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ↔ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) )
23 20 22 orbi12d ⊢ ( 𝑟 = 0 → ( ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ↔ ( 0 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
24 19 23 anbi12d ⊢ ( 𝑟 = 0 → ( ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ↔ ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) ∧ ( 0 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) )
25 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
26 8 idomringd ⊢ ( 𝜑 → 𝐹 ∈ Ring )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐹 ∈ Ring )
28 eqid ⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
29 5 flddrngd ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐹 ∈ DivRing )
31 difssd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 )
32 31 sselda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑦 ∈ 𝐵 )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑦 ∈ ( 𝐵 ∖ { 0 } ) )
34 33 eldifsnbd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑦 ≠ 0 )
35 1 2 28 30 32 34 drnginvrcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ∈ 𝐵 )
36 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
37 1 25 27 35 36 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ∈ 𝐵 )
38 26 ringgrpd ⊢ ( 𝜑 → 𝐹 ∈ Grp )
39 1 2 38 grpidcld ⊢ ( 𝜑 → 0 ∈ 𝐵 )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 0 ∈ 𝐵 )
41 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
42 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐹 ∈ Grp )
43 1 25 27 32 37 ringcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ∈ 𝐵 )
44 1 41 2 42 43 grpridd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) = ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) )
45 1 25 27 32 35 36 ringassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ) ( .r ‘ 𝐹 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) )
46 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
47 1 2 25 46 28 30 32 34 drnginvrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑦 ( .r ‘ 𝐹 ) ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ) = ( 1r ‘ 𝐹 ) )
48 47 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ) ( .r ‘ 𝐹 ) 𝑥 ) = ( ( 1r ‘ 𝐹 ) ( .r ‘ 𝐹 ) 𝑥 ) )
49 45 48 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) = ( ( 1r ‘ 𝐹 ) ( .r ‘ 𝐹 ) 𝑥 ) )
50 1 25 46 27 36 ringlidmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( 1r ‘ 𝐹 ) ( .r ‘ 𝐹 ) 𝑥 ) = 𝑥 )
51 44 49 50 3eqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) )
52 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → 0 = 0 )
53 52 orcd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 0 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) )
54 51 53 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) ( ( ( invr ‘ 𝐹 ) ‘ 𝑦 ) ( .r ‘ 𝐹 ) 𝑥 ) ) ( +g ‘ 𝐹 ) 0 ) ∧ ( 0 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 0 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
55 17 24 37 40 54 2rspcedvdw ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
56 55 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
57 56 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) )
58 13 57 jca ⊢ ( 𝜑 → ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) )
59 4 reseq1i ⊢ ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) = ( ( EuclF ‘ 𝐹 ) ↾ ( 𝐵 ∖ { 0 } ) )
60 1 2 41 25 59 isedom ⊢ ( 𝐹 ∈ EDomn ↔ ( 𝐹 ∈ IDomn ∧ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) : ( 𝐵 ∖ { 0 } ) ⟶ ℕ0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑞 ∈ 𝐵 ∃ 𝑟 ∈ 𝐵 ( 𝑥 = ( ( 𝑦 ( .r ‘ 𝐹 ) 𝑞 ) ( +g ‘ 𝐹 ) 𝑟 ) ∧ ( 𝑟 = 0 ∨ ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑟 ) < ( ( 𝐸 ↾ ( 𝐵 ∖ { 0 } ) ) ‘ 𝑦 ) ) ) ) ) )
61 8 58 60 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ EDomn )