Theorem fldgenidfld

Description: The subfield generated by a subfield is the subfield itself. (Contributed by Thierry Arnoux, 15-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
	fldgenidfld.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(F\right)$$
Assertion	fldgenidfld	$$⊢\phi \to F\mathrm{fldGen}S=S$$

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		fldgenidfld.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(F\right)$$
4	1	sdrgss	$$⊢S\in \mathrm{SubDRing}\left(F\right)\to S\subseteq B$$
5	3 4	syl	$$⊢\phi \to S\subseteq B$$
6	1 2 5	fldgenval	$$⊢\phi \to F\mathrm{fldGen}S=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}$$
7		intmin	$$⊢S\in \mathrm{SubDRing}\left(F\right)\to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}=S$$
8	3 7	syl	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|S\subseteq a\right\}=S$$
9	6 8	eqtrd	$$⊢\phi \to F\mathrm{fldGen}S=S$$