ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mulext1 Unicode version

Theorem mulext1 8631
Description: Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
Assertion
Ref Expression
mulext1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) )

Proof of Theorem mulext1
Dummy variables  u  v  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnre 8015 . . 3  |-  ( C  e.  CC  ->  E. u  e.  RR  E. v  e.  RR  C  =  ( u  +  ( _i  x.  v ) ) )
213ad2ant3 1022 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  E. u  e.  RR  E. v  e.  RR  C  =  ( u  +  ( _i  x.  v ) ) )
3 cnre 8015 . . . . . . 7  |-  ( B  e.  CC  ->  E. z  e.  RR  E. w  e.  RR  B  =  ( z  +  ( _i  x.  w ) ) )
433ad2ant2 1021 . . . . . 6  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  E. z  e.  RR  E. w  e.  RR  B  =  ( z  +  ( _i  x.  w ) ) )
54ad2antrr 488 . . . . 5  |-  ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  ->  E. z  e.  RR  E. w  e.  RR  B  =  ( z  +  ( _i  x.  w ) ) )
6 cnre 8015 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
763ad2ant1 1020 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
87adantr 276 . . . . . . . . 9  |-  ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  ( u  e.  RR  /\  v  e.  RR ) )  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
98ad3antrrr 492 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y ) ) )
10 simplrl 535 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  x  e.  RR )
1110recnd 8048 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  x  e.  CC )
12 simprl 529 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  ( u  e.  RR  /\  v  e.  RR ) )  ->  u  e.  RR )
1312ad2antrr 488 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  u  e.  RR )
1413ad3antrrr 492 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  u  e.  RR )
1514recnd 8048 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  u  e.  CC )
1611, 15mulcld 8040 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
x  x.  u )  e.  CC )
17 simplrr 536 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  y  e.  RR )
1817recnd 8048 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  y  e.  CC )
19 simprr 531 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  ( u  e.  RR  /\  v  e.  RR ) )  ->  v  e.  RR )
2019ad2antrr 488 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  v  e.  RR )
2120ad3antrrr 492 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  v  e.  RR )
2221recnd 8048 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  v  e.  CC )
2318, 22mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
y  x.  v )  e.  CC )
2423negcld 8317 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  -u (
y  x.  v )  e.  CC )
25 simprl 529 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  z  e.  RR )
2625ad3antrrr 492 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  z  e.  RR )
2726recnd 8048 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  z  e.  CC )
2827, 15mulcld 8040 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
z  x.  u )  e.  CC )
29 simprr 531 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  w  e.  RR )
3029ad3antrrr 492 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  w  e.  RR )
3130recnd 8048 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  w  e.  CC )
3231, 22mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
w  x.  v )  e.  CC )
3332negcld 8317 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  -u (
w  x.  v )  e.  CC )
34 addext 8629 . . . . . . . . . . . . . . 15  |-  ( ( ( ( x  x.  u )  e.  CC  /\  -u ( y  x.  v
)  e.  CC )  /\  ( ( z  x.  u )  e.  CC  /\  -u (
w  x.  v )  e.  CC ) )  ->  ( ( ( x  x.  u )  +  -u ( y  x.  v ) ) #  ( ( z  x.  u
)  +  -u (
w  x.  v ) )  ->  ( (
x  x.  u ) #  ( z  x.  u
)  \/  -u (
y  x.  v ) #  -u ( w  x.  v
) ) ) )
3516, 24, 28, 33, 34syl22anc 1250 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( x  x.  u )  +  -u ( y  x.  v
) ) #  ( ( z  x.  u )  +  -u ( w  x.  v ) )  -> 
( ( x  x.  u ) #  ( z  x.  u )  \/  -u ( y  x.  v
) #  -u ( w  x.  v ) ) ) )
36 remulext1 8618 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  RR  /\  z  e.  RR  /\  u  e.  RR )  ->  (
( x  x.  u
) #  ( z  x.  u )  ->  x #  z ) )
3710, 26, 14, 36syl3anc 1249 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( x  x.  u
) #  ( z  x.  u )  ->  x #  z ) )
38 apneg 8630 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  x.  v
)  e.  CC  /\  ( w  x.  v
)  e.  CC )  ->  ( ( y  x.  v ) #  ( w  x.  v )  <->  -u ( y  x.  v
) #  -u ( w  x.  v ) ) )
3923, 32, 38syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( y  x.  v
) #  ( w  x.  v )  <->  -u ( y  x.  v ) #  -u ( w  x.  v
) ) )
40 remulext1 8618 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  RR  /\  w  e.  RR  /\  v  e.  RR )  ->  (
( y  x.  v
) #  ( w  x.  v )  ->  y #  w ) )
4117, 30, 21, 40syl3anc 1249 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( y  x.  v
) #  ( w  x.  v )  ->  y #  w ) )
4239, 41sylbird 170 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  ( -u ( y  x.  v
) #  -u ( w  x.  v )  ->  y #  w ) )
4337, 42orim12d 787 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( x  x.  u ) #  ( z  x.  u )  \/  -u ( y  x.  v
) #  -u ( w  x.  v ) )  -> 
( x #  z  \/  y #  w ) ) )
4435, 43syld 45 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( x  x.  u )  +  -u ( y  x.  v
) ) #  ( ( z  x.  u )  +  -u ( w  x.  v ) )  -> 
( x #  z  \/  y #  w ) ) )
4515, 18mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
u  x.  y )  e.  CC )
4622, 11mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
v  x.  x )  e.  CC )
4715, 31mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
u  x.  w )  e.  CC )
4822, 27mulcld 8040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
v  x.  z )  e.  CC )
49 addext 8629 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( u  x.  y )  e.  CC  /\  ( v  x.  x
)  e.  CC )  /\  ( ( u  x.  w )  e.  CC  /\  ( v  x.  z )  e.  CC ) )  -> 
( ( ( u  x.  y )  +  ( v  x.  x
) ) #  ( ( u  x.  w )  +  ( v  x.  z ) )  -> 
( ( u  x.  y ) #  ( u  x.  w )  \/  ( v  x.  x
) #  ( v  x.  z ) ) ) )
5045, 46, 47, 48, 49syl22anc 1250 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w )  +  ( v  x.  z
) )  ->  (
( u  x.  y
) #  ( u  x.  w )  \/  (
v  x.  x ) #  ( v  x.  z
) ) ) )
51 remulext2 8619 . . . . . . . . . . . . . . . . 17  |-  ( ( y  e.  RR  /\  w  e.  RR  /\  u  e.  RR )  ->  (
( u  x.  y
) #  ( u  x.  w )  ->  y #  w ) )
5217, 30, 14, 51syl3anc 1249 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( u  x.  y
) #  ( u  x.  w )  ->  y #  w ) )
53 remulext2 8619 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR  /\  z  e.  RR  /\  v  e.  RR )  ->  (
( v  x.  x
) #  ( v  x.  z )  ->  x #  z ) )
5410, 26, 21, 53syl3anc 1249 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( v  x.  x
) #  ( v  x.  z )  ->  x #  z ) )
5552, 54orim12d 787 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( u  x.  y ) #  ( u  x.  w )  \/  ( v  x.  x
) #  ( v  x.  z ) )  -> 
( y #  w  \/  x #  z ) ) )
5650, 55syld 45 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w )  +  ( v  x.  z
) )  ->  (
y #  w  \/  x #  z ) ) )
57 orcom 729 . . . . . . . . . . . . . 14  |-  ( ( y #  w  \/  x #  z )  <->  ( x #  z  \/  y #  w
) )
5856, 57imbitrdi 161 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w )  +  ( v  x.  z
) )  ->  (
x #  z  \/  y #  w ) ) )
5944, 58jaod 718 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( ( x  x.  u )  + 
-u ( y  x.  v ) ) #  ( ( z  x.  u
)  +  -u (
w  x.  v ) )  \/  ( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w
)  +  ( v  x.  z ) ) )  ->  ( x #  z  \/  y #  w
) ) )
60 simpr 110 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  A  =  ( x  +  ( _i  x.  y
) ) )
61 simplr 528 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  C  =  ( u  +  (
_i  x.  v )
) )
6261ad3antrrr 492 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  C  =  ( u  +  ( _i  x.  v
) ) )
6360, 62oveq12d 5936 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  ( A  x.  C )  =  ( ( x  +  ( _i  x.  y ) )  x.  ( u  +  ( _i  x.  v ) ) ) )
64 simpllr 534 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  B  =  ( z  +  ( _i  x.  w
) ) )
6564, 62oveq12d 5936 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  ( B  x.  C )  =  ( ( z  +  ( _i  x.  w ) )  x.  ( u  +  ( _i  x.  v ) ) ) )
6663, 65breq12d 4042 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  <->  ( (
x  +  ( _i  x.  y ) )  x.  ( u  +  ( _i  x.  v
) ) ) #  ( ( z  +  ( _i  x.  w ) )  x.  ( u  +  ( _i  x.  v ) ) ) ) )
67 mulreim 8623 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( u  e.  RR  /\  v  e.  RR ) )  -> 
( ( x  +  ( _i  x.  y
) )  x.  (
u  +  ( _i  x.  v ) ) )  =  ( ( ( x  x.  u
)  +  -u (
y  x.  v ) )  +  ( _i  x.  ( ( u  x.  y )  +  ( v  x.  x
) ) ) ) )
6810, 17, 14, 21, 67syl22anc 1250 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( x  +  ( _i  x.  y ) )  x.  ( u  +  ( _i  x.  v ) ) )  =  ( ( ( x  x.  u )  +  -u ( y  x.  v ) )  +  ( _i  x.  (
( u  x.  y
)  +  ( v  x.  x ) ) ) ) )
69 mulreim 8623 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  RR  /\  w  e.  RR )  /\  ( u  e.  RR  /\  v  e.  RR ) )  -> 
( ( z  +  ( _i  x.  w
) )  x.  (
u  +  ( _i  x.  v ) ) )  =  ( ( ( z  x.  u
)  +  -u (
w  x.  v ) )  +  ( _i  x.  ( ( u  x.  w )  +  ( v  x.  z
) ) ) ) )
7026, 30, 14, 21, 69syl22anc 1250 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( z  +  ( _i  x.  w ) )  x.  ( u  +  ( _i  x.  v ) ) )  =  ( ( ( z  x.  u )  +  -u ( w  x.  v ) )  +  ( _i  x.  (
( u  x.  w
)  +  ( v  x.  z ) ) ) ) )
7168, 70breq12d 4042 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( x  +  ( _i  x.  y
) )  x.  (
u  +  ( _i  x.  v ) ) ) #  ( ( z  +  ( _i  x.  w ) )  x.  ( u  +  ( _i  x.  v ) ) )  <->  ( (
( x  x.  u
)  +  -u (
y  x.  v ) )  +  ( _i  x.  ( ( u  x.  y )  +  ( v  x.  x
) ) ) ) #  ( ( ( z  x.  u )  + 
-u ( w  x.  v ) )  +  ( _i  x.  (
( u  x.  w
)  +  ( v  x.  z ) ) ) ) ) )
7210, 14remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
x  x.  u )  e.  RR )
7317, 21remulcld 8050 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
y  x.  v )  e.  RR )
7473renegcld 8399 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  -u (
y  x.  v )  e.  RR )
7572, 74readdcld 8049 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( x  x.  u
)  +  -u (
y  x.  v ) )  e.  RR )
7614, 17remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
u  x.  y )  e.  RR )
7721, 10remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
v  x.  x )  e.  RR )
7876, 77readdcld 8049 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( u  x.  y
)  +  ( v  x.  x ) )  e.  RR )
7926, 14remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
z  x.  u )  e.  RR )
8030, 21remulcld 8050 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
w  x.  v )  e.  RR )
8180renegcld 8399 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  -u (
w  x.  v )  e.  RR )
8279, 81readdcld 8049 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( z  x.  u
)  +  -u (
w  x.  v ) )  e.  RR )
8314, 30remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
u  x.  w )  e.  RR )
8421, 26remulcld 8050 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
v  x.  z )  e.  RR )
8583, 84readdcld 8049 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( u  x.  w
)  +  ( v  x.  z ) )  e.  RR )
86 apreim 8622 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( x  x.  u )  + 
-u ( y  x.  v ) )  e.  RR  /\  ( ( u  x.  y )  +  ( v  x.  x ) )  e.  RR )  /\  (
( ( z  x.  u )  +  -u ( w  x.  v
) )  e.  RR  /\  ( ( u  x.  w )  +  ( v  x.  z ) )  e.  RR ) )  ->  ( (
( ( x  x.  u )  +  -u ( y  x.  v
) )  +  ( _i  x.  ( ( u  x.  y )  +  ( v  x.  x ) ) ) ) #  ( ( ( z  x.  u )  +  -u ( w  x.  v ) )  +  ( _i  x.  (
( u  x.  w
)  +  ( v  x.  z ) ) ) )  <->  ( (
( x  x.  u
)  +  -u (
y  x.  v ) ) #  ( ( z  x.  u )  + 
-u ( w  x.  v ) )  \/  ( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w )  +  ( v  x.  z
) ) ) ) )
8775, 78, 82, 85, 86syl22anc 1250 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( ( ( x  x.  u )  + 
-u ( y  x.  v ) )  +  ( _i  x.  (
( u  x.  y
)  +  ( v  x.  x ) ) ) ) #  ( ( ( z  x.  u
)  +  -u (
w  x.  v ) )  +  ( _i  x.  ( ( u  x.  w )  +  ( v  x.  z
) ) ) )  <-> 
( ( ( x  x.  u )  + 
-u ( y  x.  v ) ) #  ( ( z  x.  u
)  +  -u (
w  x.  v ) )  \/  ( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w
)  +  ( v  x.  z ) ) ) ) )
8866, 71, 873bitrd 214 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  <->  ( (
( x  x.  u
)  +  -u (
y  x.  v ) ) #  ( ( z  x.  u )  + 
-u ( w  x.  v ) )  \/  ( ( u  x.  y )  +  ( v  x.  x ) ) #  ( ( u  x.  w )  +  ( v  x.  z
) ) ) ) )
89 apreim 8622 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  RR  /\  y  e.  RR )  /\  ( z  e.  RR  /\  w  e.  RR ) )  -> 
( ( x  +  ( _i  x.  y
) ) #  ( z  +  ( _i  x.  w ) )  <->  ( x #  z  \/  y #  w
) ) )
9010, 17, 26, 30, 89syl22anc 1250 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( x  +  ( _i  x.  y ) ) #  ( z  +  ( _i  x.  w
) )  <->  ( x #  z  \/  y #  w
) ) )
9159, 88, 903imtr4d 203 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  (
x  +  ( _i  x.  y ) ) #  ( z  +  ( _i  x.  w ) ) ) )
9260, 64breq12d 4042 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  ( A #  B  <->  ( x  +  ( _i  x.  y
) ) #  ( z  +  ( _i  x.  w ) ) ) )
9391, 92sylibrd 169 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  /\  A  =  ( x  +  (
_i  x.  y )
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) )
9493ex 115 . . . . . . . . 9  |-  ( ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  ( u  e.  RR  /\  v  e.  RR ) )  /\  C  =  ( u  +  ( _i  x.  v ) ) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  /\  (
x  e.  RR  /\  y  e.  RR )
)  ->  ( A  =  ( x  +  ( _i  x.  y
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
9594rexlimdvva 2619 . . . . . . . 8  |-  ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  ->  ( E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
969, 95mpd 13 . . . . . . 7  |-  ( ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  /\  B  =  ( z  +  ( _i  x.  w ) ) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) )
9796ex 115 . . . . . 6  |-  ( ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  /\  (
z  e.  RR  /\  w  e.  RR )
)  ->  ( B  =  ( z  +  ( _i  x.  w
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
9897rexlimdvva 2619 . . . . 5  |-  ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  ->  ( E. z  e.  RR  E. w  e.  RR  B  =  ( z  +  ( _i  x.  w
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
995, 98mpd 13 . . . 4  |-  ( ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  (
u  e.  RR  /\  v  e.  RR )
)  /\  C  =  ( u  +  (
_i  x.  v )
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) )
10099ex 115 . . 3  |-  ( ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  /\  ( u  e.  RR  /\  v  e.  RR ) )  ->  ( C  =  ( u  +  ( _i  x.  v
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
101100rexlimdvva 2619 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( E. u  e.  RR  E. v  e.  RR  C  =  ( u  +  ( _i  x.  v
) )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) ) )
1022, 101mpd 13 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  C
) #  ( B  x.  C )  ->  A #  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709    /\ w3a 980    = wceq 1364    e. wcel 2164   E.wrex 2473   class class class wbr 4029  (class class class)co 5918   CCcc 7870   RRcr 7871   _ici 7874    + caddc 7875    x. cmul 7877   -ucneg 8191   # cap 8600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-mulrcl 7971  ax-addcom 7972  ax-mulcom 7973  ax-addass 7974  ax-mulass 7975  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-1rid 7979  ax-0id 7980  ax-rnegex 7981  ax-precex 7982  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988  ax-pre-mulgt0 7989  ax-pre-mulext 7990
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-iota 5215  df-fun 5256  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-pnf 8056  df-mnf 8057  df-ltxr 8059  df-sub 8192  df-neg 8193  df-reap 8594  df-ap 8601
This theorem is referenced by:  mulext2  8632  mulext  8633  mulap0  8673  apmul1  8807
  Copyright terms: Public domain W3C validator