Metamath Proof Explorer

Theorem axmulf

Description: Multiplication is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axmulcl . This construction-dependent theorem should not be referenced directly; instead, use ax-mulf . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion axmulf 
|- x. : ( CC X. CC ) --> CC

Proof

Step Hyp Ref Expression
1 moeq 
 |-  E* z z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >.
2 1 mosubop 
 |-  E* z E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. )
3 2 mosubop 
 |-  E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) )
4 anass 
 |-  ( ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
5 4 2exbii 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
6 19.42vv 
 |-  ( E. u E. f ( x = <. w , v >. /\ ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
7 5 6 bitri 
 |-  ( E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
8 7 2exbii 
 |-  ( E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
9 8 mobii 
 |-  ( E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) <-> E* z E. w E. v ( x = <. w , v >. /\ E. u E. f ( y = <. u , f >. /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) )
10 3 9 mpbir 
 |-  E* z E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. )
11 10 moani 
 |-  E* z ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) )
12 11 funoprab 
 |-  Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
13 df-mul 
 |-  x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
14 13 funeqi 
 |-  ( Fun x. <-> Fun { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } )
15 12 14 mpbir 
 |-  Fun x.
16 13 dmeqi 
 |-  dom x. = dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
17 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) } C_ ( CC X. CC )
18 16 17 eqsstri 
 |-  dom x. C_ ( CC X. CC )
19 0ncn 
 |-  -. (/) e. CC
20 df-c 
 |-  CC = ( R. X. R. )
21 oveq1 
 |-  ( <. z , w >. = x -> ( <. z , w >. x. <. v , u >. ) = ( x x. <. v , u >. ) )
22 21 eleq1d 
 |-  ( <. z , w >. = x -> ( ( <. z , w >. x. <. v , u >. ) e. ( R. X. R. ) <-> ( x x. <. v , u >. ) e. ( R. X. R. ) ) )
23 oveq2 
 |-  ( <. v , u >. = y -> ( x x. <. v , u >. ) = ( x x. y ) )
24 23 eleq1d 
 |-  ( <. v , u >. = y -> ( ( x x. <. v , u >. ) e. ( R. X. R. ) <-> ( x x. y ) e. ( R. X. R. ) ) )
25 mulcnsr 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. x. <. v , u >. ) = <. ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) , ( ( w .R v ) +R ( z .R u ) ) >. )
26 mulclsr 
 |-  ( ( z e. R. /\ v e. R. ) -> ( z .R v ) e. R. )
27 m1r 
 |-  -1R e. R.
28 mulclsr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( w .R u ) e. R. )
29 mulclsr 
 |-  ( ( -1R e. R. /\ ( w .R u ) e. R. ) -> ( -1R .R ( w .R u ) ) e. R. )
30 27 28 29 sylancr 
 |-  ( ( w e. R. /\ u e. R. ) -> ( -1R .R ( w .R u ) ) e. R. )
31 addclsr 
 |-  ( ( ( z .R v ) e. R. /\ ( -1R .R ( w .R u ) ) e. R. ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
32 26 30 31 syl2an 
 |-  ( ( ( z e. R. /\ v e. R. ) /\ ( w e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
33 32 an4s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) e. R. )
34 mulclsr 
 |-  ( ( w e. R. /\ v e. R. ) -> ( w .R v ) e. R. )
35 mulclsr 
 |-  ( ( z e. R. /\ u e. R. ) -> ( z .R u ) e. R. )
36 addclsr 
 |-  ( ( ( w .R v ) e. R. /\ ( z .R u ) e. R. ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
37 34 35 36 syl2anr 
 |-  ( ( ( z e. R. /\ u e. R. ) /\ ( w e. R. /\ v e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
38 37 an42s 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( ( w .R v ) +R ( z .R u ) ) e. R. )
39 33 38 opelxpd 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> <. ( ( z .R v ) +R ( -1R .R ( w .R u ) ) ) , ( ( w .R v ) +R ( z .R u ) ) >. e. ( R. X. R. ) )
40 25 39 eqeltrd 
 |-  ( ( ( z e. R. /\ w e. R. ) /\ ( v e. R. /\ u e. R. ) ) -> ( <. z , w >. x. <. v , u >. ) e. ( R. X. R. ) )
41 20 22 24 40 2optocl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. ( R. X. R. ) )
42 41 20 eleqtrrdi 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
43 19 42 oprssdm 
 |-  ( CC X. CC ) C_ dom x.
44 18 43 eqssi 
 |-  dom x. = ( CC X. CC )
45 df-fn 
 |-  ( x. Fn ( CC X. CC ) <-> ( Fun x. /\ dom x. = ( CC X. CC ) ) )
46 15 44 45 mpbir2an 
 |-  x. Fn ( CC X. CC )
47 42 rgen2 
 |-  A. x e. CC A. y e. CC ( x x. y ) e. CC
48 ffnov 
 |-  ( x. : ( CC X. CC ) --> CC <-> ( x. Fn ( CC X. CC ) /\ A. x e. CC A. y e. CC ( x x. y ) e. CC ) )
49 46 47 48 mpbir2an 
 |-  x. : ( CC X. CC ) --> CC