MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsrmo Structured version   Visualization version   Unicode version

Theorem mulsrmo 9498
Description: There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
Assertion
Ref Expression
mulsrmo  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  E* z E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)
Distinct variable groups:    t, A, u, v, w, z    t, B, u, v, w, z

Proof of Theorem mulsrmo
Dummy variables  f 
g  h  q  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 enrer 9489 . . . . . . . . . . . . . . . 16  |-  ~R  Er  ( P.  X.  P. )
21a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )  ->  ~R  Er  ( P.  X.  P. ) )
3 prsrlem1 9496 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )  ->  ( (
( ( w  e. 
P.  /\  v  e.  P. )  /\  (
s  e.  P.  /\  f  e.  P. )
)  /\  ( (
u  e.  P.  /\  t  e.  P. )  /\  ( g  e.  P.  /\  h  e.  P. )
) )  /\  (
( w  +P.  f
)  =  ( v  +P.  s )  /\  ( u  +P.  h )  =  ( t  +P.  g ) ) ) )
4 mulcmpblnr 9495 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( w  e. 
P.  /\  v  e.  P. )  /\  (
s  e.  P.  /\  f  e.  P. )
)  /\  ( (
u  e.  P.  /\  t  e.  P. )  /\  ( g  e.  P.  /\  h  e.  P. )
) )  ->  (
( ( w  +P.  f )  =  ( v  +P.  s )  /\  ( u  +P.  h )  =  ( t  +P.  g ) )  ->  <. ( ( w  .P.  u )  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >.  ~R  <. ( ( s  .P.  g )  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ) )
54imp 431 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( w  e.  P.  /\  v  e.  P. )  /\  (
s  e.  P.  /\  f  e.  P. )
)  /\  ( (
u  e.  P.  /\  t  e.  P. )  /\  ( g  e.  P.  /\  h  e.  P. )
) )  /\  (
( w  +P.  f
)  =  ( v  +P.  s )  /\  ( u  +P.  h )  =  ( t  +P.  g ) ) )  ->  <. ( ( w  .P.  u )  +P.  ( v  .P.  t
) ) ,  ( ( w  .P.  t
)  +P.  ( v  .P.  u ) ) >.  ~R  <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >.
)
63, 5syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )  ->  <. ( ( w  .P.  u )  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >.  ~R  <. ( ( s  .P.  g )  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. )
72, 6erthi 7410 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )  ->  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  =  [ <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >. ]  ~R  )
87adantrlr 729 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )  ->  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  =  [ <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >. ]  ~R  )
98adantrrr 731 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  ( ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
) )  ->  [ <. ( ( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  =  [ <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >. ]  ~R  )
10 simprlr 773 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  ( ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
) )  ->  z  =  [ <. ( ( w  .P.  u )  +P.  ( v  .P.  t
) ) ,  ( ( w  .P.  t
)  +P.  ( v  .P.  u ) ) >. ]  ~R  )
11 simprrr 775 . . . . . . . . . . . 12  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  ( ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
) )  ->  q  =  [ <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >. ]  ~R  )
129, 10, 113eqtr4d 2495 . . . . . . . . . . 11  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  ( ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
) )  ->  z  =  q )
1312expr 620 . . . . . . . . . 10  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  ( (
( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )  ->  z  =  q ) )
1413exlimdvv 1780 . . . . . . . . 9  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  ( E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  )  ->  z  =  q ) )
1514exlimdvv 1780 . . . . . . . 8  |-  ( ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  ) )  /\  (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  ( E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  )  ->  z  =  q ) )
1615ex 436 . . . . . . 7  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  ( (
( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  ->  ( E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  )  ->  z  =  q ) ) )
1716exlimdvv 1780 . . . . . 6  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  ( E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  z  =  [ <. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >. ]  ~R  )  ->  ( E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )  ->  z  =  q ) ) )
1817exlimdvv 1780 . . . . 5  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  z  =  [ <. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >. ]  ~R  )  ->  ( E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )  ->  z  =  q ) ) )
1918impd 433 . . . 4  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
)  ->  z  =  q ) )
2019alrimivv 1774 . . 3  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  A. z A. q ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
)  ->  z  =  q ) )
21 opeq12 4168 . . . . . . . . . . 11  |-  ( ( w  =  s  /\  v  =  f )  -> 
<. w ,  v >.  =  <. s ,  f
>. )
2221eceq1d 7400 . . . . . . . . . 10  |-  ( ( w  =  s  /\  v  =  f )  ->  [ <. w ,  v
>. ]  ~R  =  [ <. s ,  f >. ]  ~R  )
2322eqeq2d 2461 . . . . . . . . 9  |-  ( ( w  =  s  /\  v  =  f )  ->  ( A  =  [ <. w ,  v >. ]  ~R  <->  A  =  [ <. s ,  f >. ]  ~R  ) )
2423anbi1d 711 . . . . . . . 8  |-  ( ( w  =  s  /\  v  =  f )  ->  ( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  <->  ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  ) ) )
25 simpl 459 . . . . . . . . . . . . 13  |-  ( ( w  =  s  /\  v  =  f )  ->  w  =  s )
2625oveq1d 6305 . . . . . . . . . . . 12  |-  ( ( w  =  s  /\  v  =  f )  ->  ( w  .P.  u
)  =  ( s  .P.  u ) )
27 simpr 463 . . . . . . . . . . . . 13  |-  ( ( w  =  s  /\  v  =  f )  ->  v  =  f )
2827oveq1d 6305 . . . . . . . . . . . 12  |-  ( ( w  =  s  /\  v  =  f )  ->  ( v  .P.  t
)  =  ( f  .P.  t ) )
2926, 28oveq12d 6308 . . . . . . . . . . 11  |-  ( ( w  =  s  /\  v  =  f )  ->  ( ( w  .P.  u )  +P.  (
v  .P.  t )
)  =  ( ( s  .P.  u )  +P.  ( f  .P.  t ) ) )
3025oveq1d 6305 . . . . . . . . . . . 12  |-  ( ( w  =  s  /\  v  =  f )  ->  ( w  .P.  t
)  =  ( s  .P.  t ) )
3127oveq1d 6305 . . . . . . . . . . . 12  |-  ( ( w  =  s  /\  v  =  f )  ->  ( v  .P.  u
)  =  ( f  .P.  u ) )
3230, 31oveq12d 6308 . . . . . . . . . . 11  |-  ( ( w  =  s  /\  v  =  f )  ->  ( ( w  .P.  t )  +P.  (
v  .P.  u )
)  =  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) )
3329, 32opeq12d 4174 . . . . . . . . . 10  |-  ( ( w  =  s  /\  v  =  f )  -> 
<. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >.  =  <. ( ( s  .P.  u )  +P.  ( f  .P.  t
) ) ,  ( ( s  .P.  t
)  +P.  ( f  .P.  u ) ) >.
)
3433eceq1d 7400 . . . . . . . . 9  |-  ( ( w  =  s  /\  v  =  f )  ->  [ <. ( ( w  .P.  u )  +P.  ( v  .P.  t
) ) ,  ( ( w  .P.  t
)  +P.  ( v  .P.  u ) ) >. ]  ~R  =  [ <. ( ( s  .P.  u
)  +P.  ( f  .P.  t ) ) ,  ( ( s  .P.  t )  +P.  (
f  .P.  u )
) >. ]  ~R  )
3534eqeq2d 2461 . . . . . . . 8  |-  ( ( w  =  s  /\  v  =  f )  ->  ( q  =  [ <. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >. ]  ~R  <->  q  =  [ <. ( ( s  .P.  u )  +P.  (
f  .P.  t )
) ,  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) >. ]  ~R  ) )
3624, 35anbi12d 717 . . . . . . 7  |-  ( ( w  =  s  /\  v  =  f )  ->  ( ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  q  =  [ <. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >. ]  ~R  )  <->  ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  u )  +P.  (
f  .P.  t )
) ,  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) >. ]  ~R  ) ) )
37 opeq12 4168 . . . . . . . . . . 11  |-  ( ( u  =  g  /\  t  =  h )  -> 
<. u ,  t >.  =  <. g ,  h >. )
3837eceq1d 7400 . . . . . . . . . 10  |-  ( ( u  =  g  /\  t  =  h )  ->  [ <. u ,  t
>. ]  ~R  =  [ <. g ,  h >. ]  ~R  )
3938eqeq2d 2461 . . . . . . . . 9  |-  ( ( u  =  g  /\  t  =  h )  ->  ( B  =  [ <. u ,  t >. ]  ~R  <->  B  =  [ <. g ,  h >. ]  ~R  ) )
4039anbi2d 710 . . . . . . . 8  |-  ( ( u  =  g  /\  t  =  h )  ->  ( ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  <->  ( A  =  [ <. s ,  f
>. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  ) ) )
41 simpl 459 . . . . . . . . . . . . 13  |-  ( ( u  =  g  /\  t  =  h )  ->  u  =  g )
4241oveq2d 6306 . . . . . . . . . . . 12  |-  ( ( u  =  g  /\  t  =  h )  ->  ( s  .P.  u
)  =  ( s  .P.  g ) )
43 simpr 463 . . . . . . . . . . . . 13  |-  ( ( u  =  g  /\  t  =  h )  ->  t  =  h )
4443oveq2d 6306 . . . . . . . . . . . 12  |-  ( ( u  =  g  /\  t  =  h )  ->  ( f  .P.  t
)  =  ( f  .P.  h ) )
4542, 44oveq12d 6308 . . . . . . . . . . 11  |-  ( ( u  =  g  /\  t  =  h )  ->  ( ( s  .P.  u )  +P.  (
f  .P.  t )
)  =  ( ( s  .P.  g )  +P.  ( f  .P.  h ) ) )
4643oveq2d 6306 . . . . . . . . . . . 12  |-  ( ( u  =  g  /\  t  =  h )  ->  ( s  .P.  t
)  =  ( s  .P.  h ) )
4741oveq2d 6306 . . . . . . . . . . . 12  |-  ( ( u  =  g  /\  t  =  h )  ->  ( f  .P.  u
)  =  ( f  .P.  g ) )
4846, 47oveq12d 6308 . . . . . . . . . . 11  |-  ( ( u  =  g  /\  t  =  h )  ->  ( ( s  .P.  t )  +P.  (
f  .P.  u )
)  =  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) )
4945, 48opeq12d 4174 . . . . . . . . . 10  |-  ( ( u  =  g  /\  t  =  h )  -> 
<. ( ( s  .P.  u )  +P.  (
f  .P.  t )
) ,  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) >.  =  <. ( ( s  .P.  g )  +P.  ( f  .P.  h
) ) ,  ( ( s  .P.  h
)  +P.  ( f  .P.  g ) ) >.
)
5049eceq1d 7400 . . . . . . . . 9  |-  ( ( u  =  g  /\  t  =  h )  ->  [ <. ( ( s  .P.  u )  +P.  ( f  .P.  t
) ) ,  ( ( s  .P.  t
)  +P.  ( f  .P.  u ) ) >. ]  ~R  =  [ <. ( ( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
5150eqeq2d 2461 . . . . . . . 8  |-  ( ( u  =  g  /\  t  =  h )  ->  ( q  =  [ <. ( ( s  .P.  u )  +P.  (
f  .P.  t )
) ,  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) >. ]  ~R  <->  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  ) )
5240, 51anbi12d 717 . . . . . . 7  |-  ( ( u  =  g  /\  t  =  h )  ->  ( ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  u )  +P.  (
f  .P.  t )
) ,  ( ( s  .P.  t )  +P.  ( f  .P.  u ) ) >. ]  ~R  )  <->  ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  ) ) )
5336, 52cbvex4v 2126 . . . . . 6  |-  ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  <->  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
)
5453anbi2i 700 . . . . 5  |-  ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  <->  ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t >. ]  ~R  )  /\  z  =  [ <. ( ( w  .P.  u )  +P.  (
v  .P.  t )
) ,  ( ( w  .P.  t )  +P.  ( v  .P.  u ) ) >. ]  ~R  )  /\  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. ( ( s  .P.  g )  +P.  (
f  .P.  h )
) ,  ( ( s  .P.  h )  +P.  ( f  .P.  g ) ) >. ]  ~R  ) ) )
5554imbi1i 327 . . . 4  |-  ( ( ( E. w E. v E. u E. t
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  z  =  q )  <->  ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
)  ->  z  =  q ) )
56552albii 1692 . . 3  |-  ( A. z A. q ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  z  =  q )  <->  A. z A. q ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. s E. f E. g E. h ( ( A  =  [ <. s ,  f >. ]  ~R  /\  B  =  [ <. g ,  h >. ]  ~R  )  /\  q  =  [ <. (
( s  .P.  g
)  +P.  ( f  .P.  h ) ) ,  ( ( s  .P.  h )  +P.  (
f  .P.  g )
) >. ]  ~R  )
)  ->  z  =  q ) )
5720, 56sylibr 216 . 2  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  A. z A. q ( ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  z  =  q ) )
58 eqeq1 2455 . . . . 5  |-  ( z  =  q  ->  (
z  =  [ <. ( ( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  <->  q  =  [ <. ( ( w  .P.  u )  +P.  ( v  .P.  t
) ) ,  ( ( w  .P.  t
)  +P.  ( v  .P.  u ) ) >. ]  ~R  ) )
5958anbi2d 710 . . . 4  |-  ( z  =  q  ->  (
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  <->  ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
) )
60594exbidv 1772 . . 3  |-  ( z  =  q  ->  ( E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  <->  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
) )
6160mo4 2346 . 2  |-  ( E* z E. w E. v E. u E. t
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  <->  A. z A. q ( ( E. w E. v E. u E. t
( ( A  =  [ <. w ,  v
>. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )  /\  E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  q  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)  ->  z  =  q ) )
6257, 61sylibr 216 1  |-  ( ( A  e.  ( ( P.  X.  P. ) /.  ~R  )  /\  B  e.  ( ( P.  X.  P. ) /.  ~R  )
)  ->  E* z E. w E. v E. u E. t ( ( A  =  [ <. w ,  v >. ]  ~R  /\  B  =  [ <. u ,  t
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  t ) ) ,  ( ( w  .P.  t )  +P.  (
v  .P.  u )
) >. ]  ~R  )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1442    = wceq 1444   E.wex 1663    e. wcel 1887   E*wmo 2300   <.cop 3974   class class class wbr 4402    X. cxp 4832  (class class class)co 6290    Er wer 7360   [cec 7361   /.cqs 7362   P.cnp 9284    +P. cpp 9286    .P. cmp 9287    ~R cer 9289
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-omul 7187  df-er 7363  df-ec 7365  df-qs 7369  df-ni 9297  df-pli 9298  df-mi 9299  df-lti 9300  df-plpq 9333  df-mpq 9334  df-ltpq 9335  df-enq 9336  df-nq 9337  df-erq 9338  df-plq 9339  df-mq 9340  df-1nq 9341  df-rq 9342  df-ltnq 9343  df-np 9406  df-plp 9408  df-mp 9409  df-ltp 9410  df-enr 9480
This theorem is referenced by:  mulsrpr  9500
  Copyright terms: Public domain W3C validator