This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulnzcnf

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

Ref Expression
Assertion mulnzcnf ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } )

Proof

Step Hyp Ref Expression
1 ax-mulf ⊢ · : ( ℂ × ℂ ) ⟶ ℂ
2 ffnov ⊢ ( · : ( ℂ × ℂ ) ⟶ ℂ ↔ ( · Fn ( ℂ × ℂ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 · 𝑦 ) ∈ ℂ ) )
3 1 2 mpbi ⊢ ( · Fn ( ℂ × ℂ ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( 𝑥 · 𝑦 ) ∈ ℂ )
4 3 simpli ⊢ · Fn ( ℂ × ℂ )
5 difss ⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
6 xpss12 ⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⊆ ( ℂ × ℂ ) )
7 5 5 6 mp2an ⊢ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⊆ ( ℂ × ℂ )
8 fnssres ⊢ ( ( · Fn ( ℂ × ℂ ) ∧ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⊆ ( ℂ × ℂ ) ) → ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) Fn ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) )
9 4 7 8 mp2an ⊢ ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) Fn ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) )
10 ovres ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
11 eldifsn ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
12 eldifsn ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
13 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
14 13 ad2ant2r ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
15 mulne0 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
16 14 15 jca ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
17 11 12 16 syl2anb ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
18 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
19 17 18 sylibr ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
20 10 19 eqeltrd ⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
21 20 rgen2 ⊢ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( 𝑥 ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) ∈ ( ℂ ∖ { 0 } )
22 ffnov ⊢ ( ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } ) ↔ ( ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) Fn ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ∧ ∀ 𝑥 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑦 ∈ ( ℂ ∖ { 0 } ) ( 𝑥 ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) 𝑦 ) ∈ ( ℂ ∖ { 0 } ) ) )
23 9 21 22 mpbir2an ⊢ ( · ↾ ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } )