Theorem fldgenssp

Description: The field generated by a set of elements in a division ring is contained in any sub-division-ring which contains those elements. (Contributed by Thierry Arnoux, 25-Feb-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)$$
	fldgenssp.t	$$⊢\phi \to T\subseteq S$$
Assertion	fldgenssp	$$⊢\phi \to F\mathrm{fldGen}T\subseteq 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		fldgenssp.t	$$⊢\phi \to T\subseteq S$$
5		issdrg	$$⊢S\in \mathrm{SubDRing}\left(F\right)\leftrightarrow \left(F\in \mathrm{DivRing}\wedge S\in \mathrm{SubRing}\left(F\right)\wedge F{\upharpoonright }_{𝑠}S\in \mathrm{DivRing}\right)$$
6	3 5	sylib	$$⊢\phi \to \left(F\in \mathrm{DivRing}\wedge S\in \mathrm{SubRing}\left(F\right)\wedge F{\upharpoonright }_{𝑠}S\in \mathrm{DivRing}\right)$$
7	6	simp2d	$$⊢\phi \to S\in \mathrm{SubRing}\left(F\right)$$
8	1	subrgss	$$⊢S\in \mathrm{SubRing}\left(F\right)\to S\subseteq B$$
9	7 8	syl	$$⊢\phi \to S\subseteq B$$
10	4 9	sstrd	$$⊢\phi \to T\subseteq B$$
11	1 2 10	fldgenval	$$⊢\phi \to F\mathrm{fldGen}T=\bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}$$
12		sseq2	$$⊢a=S\to \left(T\subseteq a\leftrightarrow T\subseteq S\right)$$
13	12 3 4	elrabd	$$⊢\phi \to S\in \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}$$
14		intss1	$$⊢S\in \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\subseteq S$$
15	13 14	syl	$$⊢\phi \to \bigcap \left\{a\in \mathrm{SubDRing}\left(F\right)|T\subseteq a\right\}\subseteq S$$
16	11 15	eqsstrd	$$⊢\phi \to F\mathrm{fldGen}T\subseteq S$$