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

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

Proof

Step Hyp Ref Expression
1 fldgenval.1 ⊢ 𝐵 = ( Base ‘ 𝐹 )
2 fldgenval.2 ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
3 fldgenval.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
4 1 2 3 fldgenval ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) = ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
5 2 drngringd ⊢ ( 𝜑 → 𝐹 ∈ Ring )
6 eqid ⊢ ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) = ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
7 sseq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝑥 ) )
8 7 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ↔ ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) ∧ 𝑆 ⊆ 𝑥 ) )
9 8 biimpi ⊢ ( 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } → ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) ∧ 𝑆 ⊆ 𝑥 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) → ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) ∧ 𝑆 ⊆ 𝑥 ) )
11 10 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) → 𝑥 ∈ ( SubDRing ‘ 𝐹 ) )
12 issdrg ⊢ ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ 𝑥 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑥 ) ∈ DivRing ) )
13 12 simp2bi ⊢ ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) → 𝑥 ∈ ( SubRing ‘ 𝐹 ) )
14 11 13 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) → 𝑥 ∈ ( SubRing ‘ 𝐹 ) )
15 14 ex ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } → 𝑥 ∈ ( SubRing ‘ 𝐹 ) ) )
16 15 ssrdv ⊢ ( 𝜑 → { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ ( SubRing ‘ 𝐹 ) )
17 sseq2 ⊢ ( 𝑎 = 𝐵 → ( 𝑆 ⊆ 𝑎 ↔ 𝑆 ⊆ 𝐵 ) )
18 1 sdrgid ⊢ ( 𝐹 ∈ DivRing → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
19 2 18 syl ⊢ ( 𝜑 → 𝐵 ∈ ( SubDRing ‘ 𝐹 ) )
20 17 19 3 elrabd ⊢ ( 𝜑 → 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
21 20 ne0d ⊢ ( 𝜑 → { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ≠ ∅ )
22 12 simp3bi ⊢ ( 𝑥 ∈ ( SubDRing ‘ 𝐹 ) → ( 𝐹 ↾s 𝑥 ) ∈ DivRing )
23 11 22 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) → ( 𝐹 ↾s 𝑥 ) ∈ DivRing )
24 6 2 16 21 23 subdrgint ⊢ ( 𝜑 → ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ∈ DivRing )
25 24 drngringd ⊢ ( 𝜑 → ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ∈ Ring )
26 intss1 ⊢ ( 𝐵 ∈ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
27 20 26 syl ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 )
28 issdrg ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ 𝑎 ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s 𝑎 ) ∈ DivRing ) )
29 28 simp2bi ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐹 ) → 𝑎 ∈ ( SubRing ‘ 𝐹 ) )
30 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
31 30 subrg1cl ⊢ ( 𝑎 ∈ ( SubRing ‘ 𝐹 ) → ( 1r ‘ 𝐹 ) ∈ 𝑎 )
32 29 31 syl ⊢ ( 𝑎 ∈ ( SubDRing ‘ 𝐹 ) → ( 1r ‘ 𝐹 ) ∈ 𝑎 )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ) ∧ 𝑆 ⊆ 𝑎 ) → ( 1r ‘ 𝐹 ) ∈ 𝑎 )
34 33 ex ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ) → ( 𝑆 ⊆ 𝑎 → ( 1r ‘ 𝐹 ) ∈ 𝑎 ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ( 𝑆 ⊆ 𝑎 → ( 1r ‘ 𝐹 ) ∈ 𝑎 ) )
36 fvex ⊢ ( 1r ‘ 𝐹 ) ∈ V
37 36 elintrab ⊢ ( ( 1r ‘ 𝐹 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ↔ ∀ 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ( 𝑆 ⊆ 𝑎 → ( 1r ‘ 𝐹 ) ∈ 𝑎 ) )
38 35 37 sylibr ⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } )
39 1 30 issubrg ⊢ ( ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubRing ‘ 𝐹 ) ↔ ( ( 𝐹 ∈ Ring ∧ ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ∈ Ring ) ∧ ( ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 ∧ ( 1r ‘ 𝐹 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ) )
40 39 biimpri ⊢ ( ( ( 𝐹 ∈ Ring ∧ ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ∈ Ring ) ∧ ( ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ⊆ 𝐵 ∧ ( 1r ‘ 𝐹 ) ∈ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ) → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubRing ‘ 𝐹 ) )
41 5 25 27 38 40 syl22anc ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubRing ‘ 𝐹 ) )
42 issdrg ⊢ ( ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubDRing ‘ 𝐹 ) ↔ ( 𝐹 ∈ DivRing ∧ ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubRing ‘ 𝐹 ) ∧ ( 𝐹 ↾s ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ) ∈ DivRing ) )
43 2 41 24 42 syl3anbrc ⊢ ( 𝜑 → ∩ { 𝑎 ∈ ( SubDRing ‘ 𝐹 ) ∣ 𝑆 ⊆ 𝑎 } ∈ ( SubDRing ‘ 𝐹 ) )
44 4 43 eqeltrd ⊢ ( 𝜑 → ( 𝐹 fldGen 𝑆 ) ∈ ( SubDRing ‘ 𝐹 ) )