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