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 e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) )
2		ovex	|- ( x x. y ) e. _V
3	1 2	fnmpoi	|- ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) Fn ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) )
4		oveq12	|- ( ( x = u /\ y = v ) -> ( x x. y ) = ( u x. v ) )
5		ovex	|- ( u x. v ) e. _V
6	4 1 5	ovmpoa	|- ( ( u e. ( CC \ { 0 } ) /\ v e. ( CC \ { 0 } ) ) -> ( u ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) v ) = ( u x. v ) )
7		eldifsn	|- ( u e. ( CC \ { 0 } ) <-> ( u e. CC /\ u =/= 0 ) )
8		eldifsn	|- ( v e. ( CC \ { 0 } ) <-> ( v e. CC /\ v =/= 0 ) )
9		mulcl	|- ( ( u e. CC /\ v e. CC ) -> ( u x. v ) e. CC )
10	9	ad2ant2r	|- ( ( ( u e. CC /\ u =/= 0 ) /\ ( v e. CC /\ v =/= 0 ) ) -> ( u x. v ) e. CC )
11		mulne0	|- ( ( ( u e. CC /\ u =/= 0 ) /\ ( v e. CC /\ v =/= 0 ) ) -> ( u x. v ) =/= 0 )
12	10 11	jca	|- ( ( ( u e. CC /\ u =/= 0 ) /\ ( v e. CC /\ v =/= 0 ) ) -> ( ( u x. v ) e. CC /\ ( u x. v ) =/= 0 ) )
13	7 8 12	syl2anb	|- ( ( u e. ( CC \ { 0 } ) /\ v e. ( CC \ { 0 } ) ) -> ( ( u x. v ) e. CC /\ ( u x. v ) =/= 0 ) )
14		eldifsn	|- ( ( u x. v ) e. ( CC \ { 0 } ) <-> ( ( u x. v ) e. CC /\ ( u x. v ) =/= 0 ) )
15	13 14	sylibr	|- ( ( u e. ( CC \ { 0 } ) /\ v e. ( CC \ { 0 } ) ) -> ( u x. v ) e. ( CC \ { 0 } ) )
16	6 15	eqeltrd	|- ( ( u e. ( CC \ { 0 } ) /\ v e. ( CC \ { 0 } ) ) -> ( u ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) v ) e. ( CC \ { 0 } ) )
17	16	rgen2	|- A. u e. ( CC \ { 0 } ) A. v e. ( CC \ { 0 } ) ( u ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) v ) e. ( CC \ { 0 } )
18		ffnov	|- ( ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } ) <-> ( ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) Fn ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) /\ A. u e. ( CC \ { 0 } ) A. v e. ( CC \ { 0 } ) ( u ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) v ) e. ( CC \ { 0 } ) ) )
19	3 17 18	mpbir2an	|- ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( x x. y ) ) : ( ( CC \ { 0 } ) X. ( CC \ { 0 } ) ) --> ( CC \ { 0 } )