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 ‘ 𝐹 ) )