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

Metamath Proof Explorer

Theorem fldgenssp

Description: The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-2025)

Ref Expression
Hypotheses fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
fldgenidfld.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝐹 ) )
fldgenssp.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
Assertion fldgenssp ( 𝜑 → ( 𝐹 fldGen 𝑇 ) ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
2 fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3 fldgenidfld.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝐹 ) )
4 fldgenssp.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
5 issdrg ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑆 ) ∈ DivRing ) )
6 3 5 sylib ⊢ ( 𝜑 → ( 𝐹 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑆 ) ∈ DivRing ) )
7 6 simp2d ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝐹 ) )
8 1 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐹 ) → 𝑆 ⊆ 𝐵 )
9 7 8 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
10 4 9 sstrd ⊢ ( 𝜑 → 𝑇 ⊆ 𝐵 )
11 1 2 10 fldgenval ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑇 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } )
12 sseq2 ⊢ ( 𝑎 = 𝑆 → ( 𝑇 ⊆ 𝑎 ↔ 𝑇 ⊆ 𝑆 ) )
13 12 3 4 elrabd ⊢ ( 𝜑 → 𝑆 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } )
14 intss1 ⊢ ( 𝑆 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } ⊆ 𝑆 )
15 13 14 syl ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑇 ⊆ 𝑎 } ⊆ 𝑆 )
16 11 15 eqsstrd ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑇 ) ⊆ 𝑆 )