Metamath Proof Explorer

Theorem mpomulnzcnf

Description: Multiplication maps nonzero complex numbers to nonzero complex numbers. Version of mulnzcnf using maps-to notation, which does not require ax-mulf . (Contributed by GG, 18-Apr-2025)

Ref Expression
Assertion mpomulnzcnf ⊢ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y : ℂ ∖ 0 × ℂ ∖ 0 ⟶ ℂ ∖ 0

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y = x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y
2 ovex ⊢ x ⁢ y ∈ V
3 1 2 fnmpoi ⊢ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y Fn ℂ ∖ 0 × ℂ ∖ 0
4 oveq12 ⊢ x = u ∧ y = v → x ⁢ y = u ⁢ v
5 ovex ⊢ u ⁢ v ∈ V
6 4 1 5 ovmpoa ⊢ u ∈ ℂ ∖ 0 ∧ v ∈ ℂ ∖ 0 → u x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y v = u ⁢ v
7 eldifsn ⊢ u ∈ ℂ ∖ 0 ↔ u ∈ ℂ ∧ u ≠ 0
8 eldifsn ⊢ v ∈ ℂ ∖ 0 ↔ v ∈ ℂ ∧ v ≠ 0
9 mulcl ⊢ u ∈ ℂ ∧ v ∈ ℂ → u ⁢ v ∈ ℂ
10 9 ad2ant2r ⊢ u ∈ ℂ ∧ u ≠ 0 ∧ v ∈ ℂ ∧ v ≠ 0 → u ⁢ v ∈ ℂ
11 mulne0 ⊢ u ∈ ℂ ∧ u ≠ 0 ∧ v ∈ ℂ ∧ v ≠ 0 → u ⁢ v ≠ 0
12 10 11 jca ⊢ u ∈ ℂ ∧ u ≠ 0 ∧ v ∈ ℂ ∧ v ≠ 0 → u ⁢ v ∈ ℂ ∧ u ⁢ v ≠ 0
13 7 8 12 syl2anb ⊢ u ∈ ℂ ∖ 0 ∧ v ∈ ℂ ∖ 0 → u ⁢ v ∈ ℂ ∧ u ⁢ v ≠ 0
14 eldifsn ⊢ u ⁢ v ∈ ℂ ∖ 0 ↔ u ⁢ v ∈ ℂ ∧ u ⁢ v ≠ 0
15 13 14 sylibr ⊢ u ∈ ℂ ∖ 0 ∧ v ∈ ℂ ∖ 0 → u ⁢ v ∈ ℂ ∖ 0
16 6 15 eqeltrd ⊢ u ∈ ℂ ∖ 0 ∧ v ∈ ℂ ∖ 0 → u x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y v ∈ ℂ ∖ 0
17 16 rgen2 ⊢ ∀ u ∈ ℂ ∖ 0 ∀ v ∈ ℂ ∖ 0 u x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y v ∈ ℂ ∖ 0
18 ffnov ⊢ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y : ℂ ∖ 0 × ℂ ∖ 0 ⟶ ℂ ∖ 0 ↔ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y Fn ℂ ∖ 0 × ℂ ∖ 0 ∧ ∀ u ∈ ℂ ∖ 0 ∀ v ∈ ℂ ∖ 0 u x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y v ∈ ℂ ∖ 0
19 3 17 18 mpbir2an ⊢ x ∈ ℂ ∖ 0 , y ∈ ℂ ∖ 0 ⟼ x ⁢ y : ℂ ∖ 0 × ℂ ∖ 0 ⟶ ℂ ∖ 0