This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldgenssv

Description: A generated subfield is a subset of the field's base. (Contributed by Thierry Arnoux, 25-Feb-2025)

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

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 sseq2 ⊢ a = B → S ⊆ a ↔ S ⊆ B
6 1 sdrgid ⊢ F ∈ DivRing → B ∈ SubDRing ⁡ F
7 2 6 syl ⊢ φ → B ∈ SubDRing ⁡ F
8 5 7 3 elrabd ⊢ φ → B ∈ a ∈ SubDRing ⁡ F | S ⊆ a
9 intss1 ⊢ B ∈ a ∈ SubDRing ⁡ F | S ⊆ a → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B
10 8 9 syl ⊢ φ → ⋂ a ∈ SubDRing ⁡ F | S ⊆ a ⊆ B
11 4 10 eqsstrd ⊢ φ → F fldGen S ⊆ B