Theorem itgoss

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

	Ref	Expression
Assertion	itgoss	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑆 ) ⊆ ( IntgOver ‘ 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		plyss	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ 𝑇 ) )
2		ssrexv	⊢ ( ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ 𝑇 ) → ( ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
3	1 2	syl	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
4	3	ralrimivw	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ∀ 𝑎 ∈ ℂ ( ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
5		ss2rab	⊢ ( { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ⊆ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ↔ ∀ 𝑎 ∈ ℂ ( ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
6	4 5	sylibr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ⊆ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
7		sstr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
8		itgoval	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
9	7 8	syl	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑆 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
10		itgoval	⊢ ( 𝑇 ⊆ ℂ → ( IntgOver ‘ 𝑇 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
11	10	adantl	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑇 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
12	6 9 11	3sstr4d	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑆 ) ⊆ ( IntgOver ‘ 𝑇 ) )