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 adantr 
 |-  ( ( ( S C_ T /\ T C_ CC ) /\ 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 4 ss2rabdv 
 |-  ( ( 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 ) } )
6 sstr 
 |-  ( ( S C_ T /\ T C_ CC ) -> S C_ CC )
7 itgoval 
 |-  ( S C_ CC -> ( IntgOver ` S ) = { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
8 6 7 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 ) } )
9 itgoval 
 |-  ( T C_ CC -> ( IntgOver ` T ) = { a e. CC | E. b e. ( Poly ` T ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
10 9 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 ) } )
11 5 8 10 3sstr4d 
 |-  ( ( S C_ T /\ T C_ CC ) -> ( IntgOver ` S ) C_ ( IntgOver ` T ) )