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 ×0×0:0×00

Proof

Step Hyp Ref Expression
1 ax-mulf ×:×
2 ffnov ×:××Fn×xyxy
3 1 2 mpbi ×Fn×xyxy
4 3 simpli ×Fn×
5 difss 0
6 xpss12 000×0×
7 5 5 6 mp2an 0×0×
8 fnssres ×Fn×0×0××0×0Fn0×0
9 4 7 8 mp2an ×0×0Fn0×0
10 ovres x0y0x×0×0y=xy
11 eldifsn x0xx0
12 eldifsn y0yy0
13 mulcl xyxy
14 13 ad2ant2r xx0yy0xy
15 mulne0 xx0yy0xy0
16 14 15 jca xx0yy0xyxy0
17 11 12 16 syl2anb x0y0xyxy0
18 eldifsn xy0xyxy0
19 17 18 sylibr x0y0xy0
20 10 19 eqeltrd x0y0x×0×0y0
21 20 rgen2 x0y0x×0×0y0
22 ffnov ×0×0:0×00×0×0Fn0×0x0y0x×0×0y0
23 9 21 22 mpbir2an ×0×0:0×00