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 C_ T /\ T C_ CC ) -> ( IntgOver ` S ) C_ ( IntgOver ` T ) )

Proof

Step Hyp Ref Expression
1 plyss 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( Poly ` S ) C_ ( Poly ` T ) )
2 ssrexv 
 |-  ( ( Poly ` S ) C_ ( Poly ` T ) -> ( E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) -> E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
3 1 2 syl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) -> E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
4 3 ralrimivw 
 |-  ( ( S C_ T /\ T C_ CC ) -> A. a e. CC ( E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) -> E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
5 ss2rab 
 |-  ( { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } C_ { a e. CC | E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } <-> A. a e. CC ( E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) -> E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
6 4 5 sylibr 
 |-  ( ( S C_ T /\ T C_ CC ) -> { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } C_ { a e. CC | E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
7 sstr 
 |-  ( ( S C_ T /\ T C_ CC ) -> S C_ CC )
8 itgoval 
 |-  ( S C_ CC -> ( IntgOver ` S ) = { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
9 7 8 syl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( IntgOver ` S ) = { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
10 itgoval 
 |-  ( T C_ CC -> ( IntgOver ` T ) = { a e. CC | E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
11 10 adantl 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( IntgOver ` T ) = { a e. CC | E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
12 6 9 11 3sstr4d 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( IntgOver ` S ) C_ ( IntgOver ` T ) )