Metamath Proof Explorer

Theorem mulcnsr

Description: Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcnsr 
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. x. <. C , D >. ) = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. e. _V
2 oveq1 
 |-  ( w = A -> ( w .R u ) = ( A .R u ) )
3 oveq1 
 |-  ( v = B -> ( v .R f ) = ( B .R f ) )
4 3 oveq2d 
 |-  ( v = B -> ( -1R .R ( v .R f ) ) = ( -1R .R ( B .R f ) ) )
5 2 4 oveqan12d 
 |-  ( ( w = A /\ v = B ) -> ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) = ( ( A .R u ) +R ( -1R .R ( B .R f ) ) ) )
6 oveq1 
 |-  ( v = B -> ( v .R u ) = ( B .R u ) )
7 oveq1 
 |-  ( w = A -> ( w .R f ) = ( A .R f ) )
8 6 7 oveqan12rd 
 |-  ( ( w = A /\ v = B ) -> ( ( v .R u ) +R ( w .R f ) ) = ( ( B .R u ) +R ( A .R f ) ) )
9 5 8 opeq12d 
 |-  ( ( w = A /\ v = B ) -> <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. = <. ( ( A .R u ) +R ( -1R .R ( B .R f ) ) ) , ( ( B .R u ) +R ( A .R f ) ) >. )
10 oveq2 
 |-  ( u = C -> ( A .R u ) = ( A .R C ) )
11 oveq2 
 |-  ( f = D -> ( B .R f ) = ( B .R D ) )
12 11 oveq2d 
 |-  ( f = D -> ( -1R .R ( B .R f ) ) = ( -1R .R ( B .R D ) ) )
13 10 12 oveqan12d 
 |-  ( ( u = C /\ f = D ) -> ( ( A .R u ) +R ( -1R .R ( B .R f ) ) ) = ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) )
14 oveq2 
 |-  ( u = C -> ( B .R u ) = ( B .R C ) )
15 oveq2 
 |-  ( f = D -> ( A .R f ) = ( A .R D ) )
16 14 15 oveqan12d 
 |-  ( ( u = C /\ f = D ) -> ( ( B .R u ) +R ( A .R f ) ) = ( ( B .R C ) +R ( A .R D ) ) )
17 13 16 opeq12d 
 |-  ( ( u = C /\ f = D ) -> <. ( ( A .R u ) +R ( -1R .R ( B .R f ) ) ) , ( ( B .R u ) +R ( A .R f ) ) >. = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )
18 9 17 sylan9eq 
 |-  ( ( ( w = A /\ v = B ) /\ ( u = C /\ f = D ) ) -> <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )
19 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 ) ) >. ) ) }
20 df-c 
 |-  CC = ( R. X. R. )
21 20 eleq2i 
 |-  ( x e. CC <-> x e. ( R. X. R. ) )
22 20 eleq2i 
 |-  ( y e. CC <-> y e. ( R. X. R. ) )
23 21 22 anbi12i 
 |-  ( ( x e. CC /\ y e. CC ) <-> ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) )
24 23 anbi1i 
 |-  ( ( ( 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 ) ) >. ) ) <-> ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ 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 ) ) >. ) ) )
25 24 oprabbii 
 |-  { <. <. 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 ) ) >. ) ) } = { <. <. x , y >. , z >. | ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ 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 ) ) >. ) ) }
26 19 25 eqtri 
 |-  x. = { <. <. x , y >. , z >. | ( ( x e. ( R. X. R. ) /\ y e. ( R. X. R. ) ) /\ 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 ) ) >. ) ) }
27 1 18 26 ov3 
 |-  ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. x. <. C , D >. ) = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )