Metamath Proof Explorer

Theorem quotcl2

Description: Closure of the quotient function. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion quotcl2 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) e. ( Poly ` CC ) )

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
2 1 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
3 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
4 3 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
5 reccl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
6 5 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
7 neg1cn 
 |-  -u 1 e. CC
8 7 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> -u 1 e. CC )
9 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
10 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` S ) )
11 9 10 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` CC ) )
12 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` S ) )
13 9 12 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` CC ) )
14 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G =/= 0p )
15 2 4 6 8 11 13 14 quotcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) e. ( Poly ` CC ) )