Metamath Proof Explorer

Theorem fldgenval

Description: Value of the field generating function: ( F fldGen S ) is the smallest sub-division-ring of F containing S . (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Hypotheses fldgenval.1 ⊢ B = Base F
fldgenval.2 ⊢ φ → F ∈ DivRing
fldgenval.3 ⊢ φ → S ⊆ B
Assertion fldgenval ⊢ φ → F fldGen S = ⋂ a ∈ SubDRing ⁡ F | S ⊆ a

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ B = Base F
2 fldgenval.2 ⊢ φ → F ∈ DivRing
3 fldgenval.3 ⊢ φ → S ⊆ B
4 2 elexd ⊢ φ → F ∈ V
5 1 fvexi ⊢ B ∈ V
6 5 a1i ⊢ φ → B ∈ V
7 6 3 ssexd ⊢ φ → S ∈ V
8 1 sdrgid ⊢ F ∈ DivRing → B ∈ SubDRing ⁡ F
9 2 8 syl ⊢ φ → B ∈ SubDRing ⁡ F
10 sseq2 ⊢ a = B → S ⊆ a ↔ S ⊆ B
11 10 adantl ⊢ φ ∧ a = B → S ⊆ a ↔ S ⊆ B
12 9 11 3 rspcedvd ⊢ φ → ∃ a ∈ SubDRing ⁡ F S ⊆ a
13 intexrab ⊢ ∃ a ∈ SubDRing ⁡ F S ⊆ a ↔ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ V
14 12 13 sylib ⊢ φ → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ V
15 simpl ⊢ f = F ∧ s = S → f = F
16 15 fveq2d ⊢ f = F ∧ s = S → SubDRing ⁡ f = SubDRing ⁡ F
17 simpr ⊢ f = F ∧ s = S → s = S
18 17 sseq1d ⊢ f = F ∧ s = S → s ⊆ a ↔ S ⊆ a
19 16 18 rabeqbidv ⊢ f = F ∧ s = S → a ∈ SubDRing ⁡ f | s ⊆ a = a ∈ SubDRing ⁡ F | S ⊆ a
20 19 inteqd ⊢ f = F ∧ s = S → ⋂ a ∈ SubDRing ⁡ f | s ⊆ a = ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
21 df-fldgen ⊢ fldGen = f ∈ V , s ∈ V ⟼ ⋂ a ∈ SubDRing ⁡ f | s ⊆ a
22 20 21 ovmpoga ⊢ F ∈ V ∧ S ∈ V ∧ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ V → F fldGen S = ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
23 4 7 14 22 syl3anc ⊢ φ → F fldGen S = ⋂ a ∈ SubDRing ⁡ F | S ⊆ a