Metamath Proof Explorer

Theorem itgoss

Description: An integral element is integral over a subset. (Contributed by Stefan O'Rear, 27-Nov-2014)

		Ref	Expression
	Assertion	itgoss	$⊢ (S \subseteq T \land T \subseteq ℂ) \to IntgOver (S) \subseteq IntgOver (T)$

Proof

Step	Hyp	Ref	Expression
1		plyss	$⊢ (S \subseteq T \land T \subseteq ℂ) \to Poly (S) \subseteq Poly (T)$
2		ssrexv	$⊢ Poly (S) \subseteq Poly (T) \to (\exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1) \to \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1))$
3	1 2	syl	$⊢ (S \subseteq T \land T \subseteq ℂ) \to (\exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1) \to \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1))$
4	3	adantr	$⊢ ((S \subseteq T \land T \subseteq ℂ) \land a \in ℂ) \to (\exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1) \to \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1))$
5	4	ss2rabdv	$⊢ (S \subseteq T \land T \subseteq ℂ) \to \{a \in ℂ \| \exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\} \subseteq \{a \in ℂ \| \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
6		sstr	$⊢ (S \subseteq T \land T \subseteq ℂ) \to S \subseteq ℂ$
7		itgoval	$⊢ S \subseteq ℂ \to IntgOver (S) = \{a \in ℂ \| \exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
8	6 7	syl	$⊢ (S \subseteq T \land T \subseteq ℂ) \to IntgOver (S) = \{a \in ℂ \| \exists b \in Poly (S) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
9		itgoval	$⊢ T \subseteq ℂ \to IntgOver (T) = \{a \in ℂ \| \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
10	9	adantl	$⊢ (S \subseteq T \land T \subseteq ℂ) \to IntgOver (T) = \{a \in ℂ \| \exists b \in Poly (T) (b (a) = 0 \land coeff (b) (\deg (b)) = 1)\}$
11	5 8 10	3sstr4d	$⊢ (S \subseteq T \land T \subseteq ℂ) \to IntgOver (S) \subseteq IntgOver (T)$