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	Could not format assertion : No typesetting found for |- ( ph -> ( F fldGen B ) = B ) with typecode |-

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	Could not format ( ph -> ( F fldGen B ) C_ B ) : No typesetting found for |- ( ph -> ( F fldGen B ) C_ B ) with typecode |-
5	1 2 3	fldgenssid	Could not format ( ph -> B C_ ( F fldGen B ) ) : No typesetting found for |- ( ph -> B C_ ( F fldGen B ) ) with typecode |-
6	4 5	eqssd	Could not format ( ph -> ( F fldGen B ) = B ) : No typesetting found for |- ( ph -> ( F fldGen B ) = B ) with typecode |-