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 ⊆ T ∧ T ⊆ ℂ → IntgOver ⁡ S ⊆ IntgOver ⁡ T

Proof

Step Hyp Ref Expression
1 plyss ⊢ S ⊆ T ∧ T ⊆ ℂ → Poly ⁡ S ⊆ Poly ⁡ T
2 ssrexv ⊢ Poly ⁡ S ⊆ Poly ⁡ T → ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 → ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
3 1 2 syl ⊢ S ⊆ T ∧ T ⊆ ℂ → ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 → ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
4 3 ralrimivw ⊢ S ⊆ T ∧ T ⊆ ℂ → ∀ a ∈ ℂ ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 → ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
5 ss2rab ⊢ a ∈ ℂ | ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 ⊆ a ∈ ℂ | ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 ↔ ∀ a ∈ ℂ ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 → ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
6 4 5 sylibr ⊢ S ⊆ T ∧ T ⊆ ℂ → a ∈ ℂ | ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1 ⊆ a ∈ ℂ | ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
7 sstr ⊢ S ⊆ T ∧ T ⊆ ℂ → S ⊆ ℂ
8 itgoval ⊢ S ⊆ ℂ → IntgOver ⁡ S = a ∈ ℂ | ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
9 7 8 syl ⊢ S ⊆ T ∧ T ⊆ ℂ → IntgOver ⁡ S = a ∈ ℂ | ∃ b ∈ Poly ⁡ S b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
10 itgoval ⊢ T ⊆ ℂ → IntgOver ⁡ T = a ∈ ℂ | ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
11 10 adantl ⊢ S ⊆ T ∧ T ⊆ ℂ → IntgOver ⁡ T = a ∈ ℂ | ∃ b ∈ Poly ⁡ T b ⁡ a = 0 ∧ coeff ⁡ b ⁡ deg ⁡ b = 1
12 6 9 11 3sstr4d ⊢ S ⊆ T ∧ T ⊆ ℂ → IntgOver ⁡ S ⊆ IntgOver ⁡ T