mulnzcnf

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

		Ref	Expression
	Assertion	mulnzcnf	$⊢ ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) : (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) ⟶ ℂ ∖ \{0\}$

Proof

Step	Hyp	Ref	Expression
1		ax-mulf	$⊢ \times : ℂ \times ℂ ⟶ ℂ$
2		ffnov	$⊢ \times : ℂ \times ℂ ⟶ ℂ \leftrightarrow (\times Fn (ℂ \times ℂ) \land \forall x \in ℂ \forall y \in ℂ x y \in ℂ)$
3	1 2	mpbi	$⊢ (\times Fn (ℂ \times ℂ) \land \forall x \in ℂ \forall y \in ℂ x y \in ℂ)$
4	3	simpli	$⊢ \times Fn (ℂ \times ℂ)$
5		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
6		xpss12	$⊢ (ℂ ∖ \{0\} \subseteq ℂ \land ℂ ∖ \{0\} \subseteq ℂ) \to (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) \subseteq ℂ \times ℂ$
7	5 5 6	mp2an	$⊢ (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) \subseteq ℂ \times ℂ$
8		fnssres	$⊢ (\times Fn (ℂ \times ℂ) \land (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) \subseteq ℂ \times ℂ) \to ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) Fn ((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))$
9	4 7 8	mp2an	$⊢ ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) Fn ((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))$
10		ovres	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) y = x y$
11		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
12		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
13		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
14	13	ad2ant2r	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \in ℂ$
15		mulne0	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to x y \neq 0$
16	14 15	jca	$⊢ ((x \in ℂ \land x \neq 0) \land (y \in ℂ \land y \neq 0)) \to (x y \in ℂ \land x y \neq 0)$
17	11 12 16	syl2anb	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to (x y \in ℂ \land x y \neq 0)$
18		eldifsn	$⊢ x y \in (ℂ ∖ \{0\}) \leftrightarrow (x y \in ℂ \land x y \neq 0)$
19	17 18	sylibr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in (ℂ ∖ \{0\})$
20	10 19	eqeltrd	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) y \in (ℂ ∖ \{0\})$
21	20	rgen2	$⊢ \forall x \in (ℂ ∖ \{0\}) \forall y \in (ℂ ∖ \{0\}) x ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) y \in (ℂ ∖ \{0\})$
22		ffnov	$⊢ ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) : (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) ⟶ ℂ ∖ \{0\} \leftrightarrow (({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) Fn ((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\})) \land \forall x \in (ℂ ∖ \{0\}) \forall y \in (ℂ ∖ \{0\}) x ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) y \in (ℂ ∖ \{0\}))$
23	9 21 22	mpbir2an	$⊢ ({\times ↾}_{((ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}))}) : (ℂ ∖ \{0\}) \times (ℂ ∖ \{0\}) ⟶ ℂ ∖ \{0\}$

Metamath Proof Explorer

Theorem mulnzcnf

Proof