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 ⊢ 𝐵 = ( Base ‘ 𝐹 )
fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
fldgenval.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion fldgenssv ( 𝜑 → ( 𝐹 fldGen 𝑆 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
2 fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3 fldgenval.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4 1 2 3 fldgenval ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
5 sseq2 ⊢ ( 𝑎 = 𝐵 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
6 1 sdrgid ⊢ ( 𝐹 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
7 2 6 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
8 5 7 3 elrabd ⊢ ( 𝜑 → 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
9 intss1 ⊢ ( 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
10 8 9 syl ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
11 4 10 eqsstrd ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) ⊆ 𝐵 )