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