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

Metamath Proof Explorer

Theorem fldgenval

Description: Value of the field generating function: ( F fldGen S ) is the smallest sub-division-ring of F containing S . (Contributed by Thierry Arnoux, 11-Jan-2025)

Ref Expression
Hypotheses fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
fldgenval.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
Assertion fldgenval ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
2 fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3 fldgenval.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4 2 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
5 1 fvexi ⊢ 𝐵 ∈ V
6 5 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
7 6 3 ssexd ⊢ ( 𝜑 → 𝑆 ∈ V )
8 1 sdrgid ⊢ ( 𝐹 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
9 2 8 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
10 sseq2 ⊢ ( 𝑎 = 𝐵 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑎 = 𝐵 ) → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
12 9 11 3 rspcedvd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) 𝑆 ⊆ 𝑎 )
13 intexrab ⊢ ( ∃ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) 𝑆 ⊆ 𝑎 ↔ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V )
14 12 13 sylib ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V )
15 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → 𝑓 = 𝐹 )
16 15 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ( SubDRing ‘ 𝑓 ) = ( SubDRing ‘ 𝐹 ) )
17 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
18 17 sseq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ( 𝑠 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝑎 ) )
19 16 18 rabeqbidv ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } = { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
20 19 inteqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑠 = 𝑆 ) → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
21 df-fldgen ⊢ fldGen = ( 𝑓 ∈ V , 𝑠 ∈ V ↦ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝑓 ) ∣ 𝑠 ⊆ 𝑎 } )
22 20 21 ovmpoga ⊢ ( ( 𝐹 ∈ V ∧ 𝑆 ∈ V ∧ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ V ) → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
23 4 7 14 22 syl3anc ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )