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 = ( Base ` F )
	fldgenval.2	|- ( ph -> F e. DivRing )
	fldgenidfld.s	|- ( ph -> S e. ( SubDRing ` F ) )
	fldgenssp.t	|- ( ph -> T C_ S )
Assertion	fldgenssp	|- ( ph -> ( F fldGen T ) C_ S )

Proof

Step	Hyp	Ref	Expression
1		fldgenval.1	|- B = ( Base ` F )
2		fldgenval.2	|- ( ph -> F e. DivRing )
3		fldgenidfld.s	|- ( ph -> S e. ( SubDRing ` F ) )
4		fldgenssp.t	|- ( ph -> T C_ S )
5		issdrg	|- ( S e. ( SubDRing ` F ) <-> ( F e. DivRing /\ S e. ( SubRing ` F ) /\ ( F |`s S ) e. DivRing ) )
6	3 5	sylib	|- ( ph -> ( F e. DivRing /\ S e. ( SubRing ` F ) /\ ( F |`s S ) e. DivRing ) )
7	6	simp2d	|- ( ph -> S e. ( SubRing ` F ) )
8	1	subrgss	|- ( S e. ( SubRing ` F ) -> S C_ B )
9	7 8	syl	|- ( ph -> S C_ B )
10	4 9	sstrd	|- ( ph -> T C_ B )
11	1 2 10	fldgenval	|- ( ph -> ( F fldGen T ) = |^| { a e. ( SubDRing ` F ) | T C_ a } )
12		sseq2	|- ( a = S -> ( T C_ a <-> T C_ S ) )
13	12 3 4	elrabd	|- ( ph -> S e. { a e. ( SubDRing ` F ) | T C_ a } )
14		intss1	|- ( S e. { a e. ( SubDRing ` F ) | T C_ a } -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ S )
15	13 14	syl	|- ( ph -> |^| { a e. ( SubDRing ` F ) | T C_ a } C_ S )
16	11 15	eqsstrd	|- ( ph -> ( F fldGen T ) C_ S )