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	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) )
2		ovex	⊢ ( 𝑥 · 𝑦 ) ∈ V
3	1 2	fnmpoi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) Fn ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) )
4		oveq12	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑥 · 𝑦 ) = ( 𝑢 · 𝑣 ) )
5		ovex	⊢ ( 𝑢 · 𝑣 ) ∈ V
6	4 1 5	ovmpoa	⊢ ( ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) = ( 𝑢 · 𝑣 ) )
7		eldifsn	⊢ ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) )
8		eldifsn	⊢ ( 𝑣 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑣 ∈ ℂ ∧ 𝑣 ≠ 0 ) )
9		mulcl	⊢ ( ( 𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
10	9	ad2ant2r	⊢ ( ( ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) ∧ ( 𝑣 ∈ ℂ ∧ 𝑣 ≠ 0 ) ) → ( 𝑢 · 𝑣 ) ∈ ℂ )
11		mulne0	⊢ ( ( ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) ∧ ( 𝑣 ∈ ℂ ∧ 𝑣 ≠ 0 ) ) → ( 𝑢 · 𝑣 ) ≠ 0 )
12	10 11	jca	⊢ ( ( ( 𝑢 ∈ ℂ ∧ 𝑢 ≠ 0 ) ∧ ( 𝑣 ∈ ℂ ∧ 𝑣 ≠ 0 ) ) → ( ( 𝑢 · 𝑣 ) ∈ ℂ ∧ ( 𝑢 · 𝑣 ) ≠ 0 ) )
13	7 8 12	syl2anb	⊢ ( ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑢 · 𝑣 ) ∈ ℂ ∧ ( 𝑢 · 𝑣 ) ≠ 0 ) )
14		eldifsn	⊢ ( ( 𝑢 · 𝑣 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑢 · 𝑣 ) ∈ ℂ ∧ ( 𝑢 · 𝑣 ) ≠ 0 ) )
15	13 14	sylibr	⊢ ( ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 · 𝑣 ) ∈ ( ℂ ∖ { 0 } ) )
16	6 15	eqeltrd	⊢ ( ( 𝑢 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑣 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑢 ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) ∈ ( ℂ ∖ { 0 } ) )
17	16	rgen2	⊢ ∀ 𝑢 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( 𝑢 ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) ∈ ( ℂ ∖ { 0 } )
18		ffnov	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) Fn ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ∧ ∀ 𝑢 ∈ ( ℂ ∖ { 0 } ) ∀ 𝑣 ∈ ( ℂ ∖ { 0 } ) ( 𝑢 ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) 𝑣 ) ∈ ( ℂ ∖ { 0 } ) ) )
19	3 17 18	mpbir2an	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · 𝑦 ) ) : ( ( ℂ ∖ { 0 } ) × ( ℂ ∖ { 0 } ) ) ⟶ ( ℂ ∖ { 0 } )