Metamath Proof Explorer

Theorem mulnzcnopr

Description: Multiplication maps nonzero complex numbers to nonzero complex numbers. (Contributed by Steve Rodriguez, 23-Feb-2007)

Ref Expression
Assertion mulnzcnopr 
|- ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } )

Proof

Step Hyp Ref Expression
1 ax-mulf 
 |-  x. : ( CC X. CC ) --> CC
2 ffnov 
 |-  ( x. : ( CC X. CC ) --> CC <-> ( x. Fn ( CC X. CC ) /\ A. x e. CC A. y e. CC ( x x. y ) e. CC ) )
3 1 2 mpbi 
 |-  ( x. Fn ( CC X. CC ) /\ A. x e. CC A. y e. CC ( x x. y ) e. CC )
4 3 simpli 
 |-  x. Fn ( CC X. CC )
5 difss 
 |-  ( CC \ { 0 } ) C_ CC
6 xpss12 
 |-  ( ( ( CC \ { 0 } ) C_ CC /\ ( CC \ { 0 } ) C_ CC ) -> ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) C_ ( CC X. CC ) )
7 5 5 6 mp2an 
 |-  ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) C_ ( CC X. CC )
8 fnssres 
 |-  ( ( x. Fn ( CC X. CC ) /\ ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) C_ ( CC X. CC ) ) -> ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) Fn ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) )
9 4 7 8 mp2an 
 |-  ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) Fn ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) )
10 ovres 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) = ( x x. y ) )
11 eldifsn 
 |-  ( x e. ( CC \ { 0 } ) <-> ( x e. CC /\ x =/= 0 ) )
12 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
13 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
14 13 ad2ant2r 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) e. CC )
15 mulne0 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( x x. y ) =/= 0 )
16 14 15 jca 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( y e. CC /\ y =/= 0 ) ) -> ( ( x x. y ) e. CC /\ ( x x. y ) =/= 0 ) )
17 11 12 16 syl2anb 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( ( x x. y ) e. CC /\ ( x x. y ) =/= 0 ) )
18 eldifsn 
 |-  ( ( x x. y ) e. ( CC \ { 0 } ) <-> ( ( x x. y ) e. CC /\ ( x x. y ) =/= 0 ) )
19 17 18 sylibr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. ( CC \ { 0 } ) )
20 10 19 eqeltrd 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) e. ( CC \ { 0 } ) )
21 20 rgen2 
 |-  A. x e. ( CC \ { 0 } ) A. y e. ( CC \ { 0 } ) ( x ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) e. ( CC \ { 0 } )
22 ffnov 
 |-  ( ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } ) <-> ( ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) Fn ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) /\ A. x e. ( CC \ { 0 } ) A. y e. ( CC \ { 0 } ) ( x ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) y ) e. ( CC \ { 0 } ) ) )
23 9 21 22 mpbir2an 
 |-  ( x. |` ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } )