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

Metamath Proof Explorer

Theorem mpomulf

Description: Multiplication is an operation on complex numbers. Version of ax-mulf using maps-to notation, proved from the axioms of set theory and ax-mulcl . (Contributed by GG, 16-Mar-2025)

Ref Expression
Assertion mpomulf 
|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = ( x e. CC , y e. CC |-> ( x x. y ) )
2 ovex 
 |-  ( x x. y ) e. _V
3 1 2 fnmpoi 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC )
4 simpll 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> x e. CC )
5 simplr 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> y e. CC )
6 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
7 eleq1a 
 |-  ( ( x x. y ) e. CC -> ( z = ( x x. y ) -> z e. CC ) )
8 6 7 syl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( z = ( x x. y ) -> z e. CC ) )
9 8 imp 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> z e. CC )
10 4 5 9 3jca 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) -> ( x e. CC /\ y e. CC /\ z e. CC ) )
11 10 ssoprab2i 
 |-  { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) } C_ { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
12 df-mpo 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ z = ( x x. y ) ) }
13 dfxp3 
 |-  ( ( CC X. CC ) X. CC ) = { <. <. x , y >. , z >. | ( x e. CC /\ y e. CC /\ z e. CC ) }
14 11 12 13 3sstr4i 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) C_ ( ( CC X. CC ) X. CC )
15 dff2 
 |-  ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( x e. CC , y e. CC |-> ( x x. y ) ) C_ ( ( CC X. CC ) X. CC ) ) )
16 3 14 15 mpbir2an 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC