Metamath Proof Explorer

Theorem fldgensdrg

Description: A generated subfield is a sub-division-ring. (Contributed by Thierry Arnoux, 11-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ B = Base F
2 fldgenval.2 ⊢ φ → F ∈ DivRing
3 fldgenval.3 ⊢ φ → S ⊆ B
4 1 2 3 fldgenval ⊢ φ → F fldGen S = ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
5 2 drngringd ⊢ φ → F ∈ Ring
6 eqid ⊢ F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a = F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
7 sseq2 ⊢ a = x → S ⊆ a ↔ S ⊆ x
8 7 elrab ⊢ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a ↔ x ∈ SubDRing ⁡ F ∧ S ⊆ x
9 8 biimpi ⊢ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → x ∈ SubDRing ⁡ F ∧ S ⊆ x
10 9 adantl ⊢ φ ∧ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → x ∈ SubDRing ⁡ F ∧ S ⊆ x
11 10 simpld ⊢ φ ∧ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → x ∈ SubDRing ⁡ F
12 issdrg ⊢ x ∈ SubDRing ⁡ F ↔ F ∈ DivRing ∧ x ∈ SubRing ⁡ F ∧ F ↾ 𝑠 x ∈ DivRing
13 12 simp2bi ⊢ x ∈ SubDRing ⁡ F → x ∈ SubRing ⁡ F
14 11 13 syl ⊢ φ ∧ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → x ∈ SubRing ⁡ F
15 14 ex ⊢ φ → x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → x ∈ SubRing ⁡ F
16 15 ssrdv ⊢ φ → a ∈ SubDRing ⁡ F | S ⊆ a ⊆ SubRing ⁡ F
17 sseq2 ⊢ a = B → S ⊆ a ↔ S ⊆ B
18 1 sdrgid ⊢ F ∈ DivRing → B ∈ SubDRing ⁡ F
19 2 18 syl ⊢ φ → B ∈ SubDRing ⁡ F
20 17 19 3 elrabd ⊢ φ → B ∈ a ∈ SubDRing ⁡ F | S ⊆ a
21 20 ne0d ⊢ φ → a ∈ SubDRing ⁡ F | S ⊆ a ≠ ∅
22 12 simp3bi ⊢ x ∈ SubDRing ⁡ F → F ↾ 𝑠 x ∈ DivRing
23 11 22 syl ⊢ φ ∧ x ∈ a ∈ SubDRing ⁡ F | S ⊆ a → F ↾ 𝑠 x ∈ DivRing
24 6 2 16 21 23 subdrgint ⊢ φ → F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ DivRing
25 24 drngringd ⊢ φ → F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ Ring
26 intss1 ⊢ B ∈ a ∈ SubDRing ⁡ F | S ⊆ a → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B
27 20 26 syl ⊢ φ → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B
28 issdrg ⊢ a ∈ SubDRing ⁡ F ↔ F ∈ DivRing ∧ a ∈ SubRing ⁡ F ∧ F ↾ 𝑠 a ∈ DivRing
29 28 simp2bi ⊢ a ∈ SubDRing ⁡ F → a ∈ SubRing ⁡ F
30 eqid ⊢ 1 F = 1 F
31 30 subrg1cl ⊢ a ∈ SubRing ⁡ F → 1 F ∈ a
32 29 31 syl ⊢ a ∈ SubDRing ⁡ F → 1 F ∈ a
33 32 ad2antlr ⊢ φ ∧ a ∈ SubDRing ⁡ F ∧ S ⊆ a → 1 F ∈ a
34 33 ex ⊢ φ ∧ a ∈ SubDRing ⁡ F → S ⊆ a → 1 F ∈ a
35 34 ralrimiva ⊢ φ → ∀ a ∈ SubDRing ⁡ F S ⊆ a → 1 F ∈ a
36 fvex ⊢ 1 F ∈ V
37 36 elintrab ⊢ 1 F ∈ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ↔ ∀ a ∈ SubDRing ⁡ F S ⊆ a → 1 F ∈ a
38 35 37 sylibr ⊢ φ → 1 F ∈ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
39 1 30 issubrg ⊢ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubRing ⁡ F ↔ F ∈ Ring ∧ F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ Ring ∧ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B ∧ 1 F ∈ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a
40 39 biimpri ⊢ F ∈ Ring ∧ F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ Ring ∧ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B ∧ 1 F ∈ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubRing ⁡ F
41 5 25 27 38 40 syl22anc ⊢ φ → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubRing ⁡ F
42 issdrg ⊢ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubDRing ⁡ F ↔ F ∈ DivRing ∧ ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubRing ⁡ F ∧ F ↾ 𝑠 ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ DivRing
43 2 41 24 42 syl3anbrc ⊢ φ → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ∈ SubDRing ⁡ F
44 4 43 eqeltrd ⊢ φ → F fldGen S ∈ SubDRing ⁡ F