This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to F \in DivRing$
		fldgenidfld.s	$⊢ φ \to S \in SubDRing (F)$
		fldgenssp.t	$⊢ φ \to T \subseteq S$
	Assertion	fldgenssp	$⊢ φ \to F fldGen T \subseteq S$

Proof

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		fldgenssp.t	$⊢ φ \to T \subseteq S$
5		issdrg	$⊢ S \in SubDRing (F) \leftrightarrow (F \in DivRing \land S \in SubRing (F) \land F ↾_{𝑠} S \in DivRing)$
6	3 5	sylib	$⊢ φ \to (F \in DivRing \land S \in SubRing (F) \land F ↾_{𝑠} S \in DivRing)$
7	6	simp2d	$⊢ φ \to S \in SubRing (F)$
8	1	subrgss	$⊢ S \in SubRing (F) \to S \subseteq B$
9	7 8	syl	$⊢ φ \to S \subseteq B$
10	4 9	sstrd	$⊢ φ \to T \subseteq B$
11	1 2 10	fldgenval	$⊢ φ \to F fldGen T = ⋂ \{a \in SubDRing (F) \| T \subseteq a\}$
12		sseq2	$⊢ a = S \to (T \subseteq a \leftrightarrow T \subseteq S)$
13	12 3 4	elrabd	$⊢ φ \to S \in \{a \in SubDRing (F) \| T \subseteq a\}$
14		intss1	$⊢ S \in \{a \in SubDRing (F) \| T \subseteq a\} \to ⋂ \{a \in SubDRing (F) \| T \subseteq a\} \subseteq S$
15	13 14	syl	$⊢ φ \to ⋂ \{a \in SubDRing (F) \| T \subseteq a\} \subseteq S$
16	11 15	eqsstrd	$⊢ φ \to F fldGen T \subseteq S$