Theorem itgocn

Description: All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

	Ref	Expression
Assertion	itgocn	⊢ ( IntgOver ‘ 𝑆 ) ⊆ ℂ

Proof

Step	Hyp	Ref	Expression
1		df-itgo	⊢ IntgOver = ( 𝑎 ∈ 𝒫 ℂ ↦ { 𝑏 ∈ ℂ ∣ ∃ 𝑐 ∈ ( Poly ‘ 𝑎 ) ( ( 𝑐 ‘ 𝑏 ) = 0 ∧ ( ( coeff ‘ 𝑐 ) ‘ ( deg ‘ 𝑐 ) ) = 1 ) } )
2	1	dmmptss	⊢ dom IntgOver ⊆ 𝒫 ℂ
3	2	sseli	⊢ ( 𝑆 ∈ dom IntgOver → 𝑆 ∈ 𝒫 ℂ )
4		cnex	⊢ ℂ ∈ V
5	4	elpw2	⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
6		itgoval	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
7		ssrab2	⊢ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ 𝑆 ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ⊆ ℂ
8	6 7	eqsstrdi	⊢ ( 𝑆 ⊆ ℂ → ( IntgOver ‘ 𝑆 ) ⊆ ℂ )
9	5 8	sylbi	⊢ ( 𝑆 ∈ 𝒫 ℂ → ( IntgOver ‘ 𝑆 ) ⊆ ℂ )
10	3 9	syl	⊢ ( 𝑆 ∈ dom IntgOver → ( IntgOver ‘ 𝑆 ) ⊆ ℂ )
11		ndmfv	⊢ ( ¬ 𝑆 ∈ dom IntgOver → ( IntgOver ‘ 𝑆 ) = ∅ )
12		0ss	⊢ ∅ ⊆ ℂ
13	11 12	eqsstrdi	⊢ ( ¬ 𝑆 ∈ dom IntgOver → ( IntgOver ‘ 𝑆 ) ⊆ ℂ )
14	10 13	pm2.61i	⊢ ( IntgOver ‘ 𝑆 ) ⊆ ℂ