fldgenidfld

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

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

Metamath Proof Explorer