Theorem fldgenid

Description: The subfield of a field F generated by the whole base set of F is F itself. (Contributed by Thierry Arnoux, 11-Jan-2025)

	Ref	Expression
Hypotheses	fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
	fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
Assertion	fldgenid	$$⊢\phi \to F\mathrm{fldGen}B=B$$

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	$$⊢B={\mathrm{Base}}_F$$
2		fldgenval.2	$$⊢\phi \to F\in \mathrm{DivRing}$$
3		ssidd	$$⊢\phi \to B\subseteq B$$
4	1 2 3	fldgenssv	$$⊢\phi \to F\mathrm{fldGen}B\subseteq B$$
5	1 2 3	fldgenssid	$$⊢\phi \to B\subseteq F\mathrm{fldGen}B$$
6	4 5	eqssd	$$⊢\phi \to F\mathrm{fldGen}B=B$$