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	adantr	⊢ ( ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) ∧ 𝑎 ∈ ℂ ) → ( ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
5	4	ss2rabdv	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ⊆ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
6		sstr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
7		itgoval	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
8	6 7	syl	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑆 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
9		itgoval	⊢ ( 𝑇 ⊆ ℂ → ( IntgOver ‘ 𝑇 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
10	9	adantl	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑇 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑇 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
11	5 8 10	3sstr4d	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( IntgOver ‘ 𝑆 ) ⊆ ( IntgOver ‘ 𝑇 ) )