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

Theorem ecopovtrn 6761
Description: Assuming that operation  F is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation  .~, specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypotheses
Ref Expression
ecopopr.1  |-  .~  =  { <. x ,  y
>.  |  ( (
x  e.  ( S  X.  S )  /\  y  e.  ( S  X.  S ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z 
.+  u )  =  ( w  .+  v
) ) ) }
ecopopr.com  |-  ( x 
.+  y )  =  ( y  .+  x
)
ecopopr.cl  |-  ( ( x  e.  S  /\  y  e.  S )  ->  ( x  .+  y
)  e.  S )
ecopopr.ass  |-  ( ( x  .+  y ) 
.+  z )  =  ( x  .+  (
y  .+  z )
)
ecopopr.can  |-  ( ( x  e.  S  /\  y  e.  S )  ->  ( ( x  .+  y )  =  ( x  .+  z )  ->  y  =  z ) )
Assertion
Ref Expression
ecopovtrn  |-  ( ( A  .~  B  /\  B  .~  C )  ->  A  .~  C )
Distinct variable groups:    x, y,
z, w, v, u, 
.+    x, S, y, z, w, v, u
Allowed substitution hints:    A( x, y, z, w, v, u)    B( x, y, z, w, v, u)    C( x, y, z, w, v, u)    .~ ( x, y, z, w, v, u)

Proof of Theorem ecopovtrn
Dummy variables  f 
g  h  t  s  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ecopopr.1 . . . . . . 7  |-  .~  =  { <. x ,  y
>.  |  ( (
x  e.  ( S  X.  S )  /\  y  e.  ( S  X.  S ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z 
.+  u )  =  ( w  .+  v
) ) ) }
2 opabssxp 4762 . . . . . . 7  |-  { <. x ,  y >.  |  ( ( x  e.  ( S  X.  S )  /\  y  e.  ( S  X.  S ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .+  u
)  =  ( w 
.+  v ) ) ) }  C_  (
( S  X.  S
)  X.  ( S  X.  S ) )
31, 2eqsstri 3208 . . . . . 6  |-  .~  C_  (
( S  X.  S
)  X.  ( S  X.  S ) )
43brel 4737 . . . . 5  |-  ( A  .~  B  ->  ( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S
) ) )
54simpld 445 . . . 4  |-  ( A  .~  B  ->  A  e.  ( S  X.  S
) )
63brel 4737 . . . 4  |-  ( B  .~  C  ->  ( B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S
) ) )
75, 6anim12i 549 . . 3  |-  ( ( A  .~  B  /\  B  .~  C )  -> 
( A  e.  ( S  X.  S )  /\  ( B  e.  ( S  X.  S
)  /\  C  e.  ( S  X.  S
) ) ) )
8 3anass 938 . . 3  |-  ( ( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S
) )  <->  ( A  e.  ( S  X.  S
)  /\  ( B  e.  ( S  X.  S
)  /\  C  e.  ( S  X.  S
) ) ) )
97, 8sylibr 203 . 2  |-  ( ( A  .~  B  /\  B  .~  C )  -> 
( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S ) ) )
10 eqid 2283 . . 3  |-  ( S  X.  S )  =  ( S  X.  S
)
11 breq1 4026 . . . . 5  |-  ( <.
f ,  g >.  =  A  ->  ( <.
f ,  g >.  .~  <. h ,  t
>. 
<->  A  .~  <. h ,  t >. )
)
1211anbi1d 685 . . . 4  |-  ( <.
f ,  g >.  =  A  ->  ( (
<. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  <->  ( A  .~  <.
h ,  t >.  /\  <. h ,  t
>.  .~  <. s ,  r
>. ) ) )
13 breq1 4026 . . . 4  |-  ( <.
f ,  g >.  =  A  ->  ( <.
f ,  g >.  .~  <. s ,  r
>. 
<->  A  .~  <. s ,  r >. )
)
1412, 13imbi12d 311 . . 3  |-  ( <.
f ,  g >.  =  A  ->  ( ( ( <. f ,  g
>.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  ->  <. f ,  g >.  .~  <. s ,  r >. )  <->  ( ( A  .~  <. h ,  t >.  /\  <. h ,  t >.  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )
) )
15 breq2 4027 . . . . 5  |-  ( <.
h ,  t >.  =  B  ->  ( A  .~  <. h ,  t
>. 
<->  A  .~  B ) )
16 breq1 4026 . . . . 5  |-  ( <.
h ,  t >.  =  B  ->  ( <.
h ,  t >.  .~  <. s ,  r
>. 
<->  B  .~  <. s ,  r >. )
)
1715, 16anbi12d 691 . . . 4  |-  ( <.
h ,  t >.  =  B  ->  ( ( A  .~  <. h ,  t >.  /\  <. h ,  t >.  .~  <. s ,  r >. )  <->  ( A  .~  B  /\  B  .~  <. s ,  r
>. ) ) )
1817imbi1d 308 . . 3  |-  ( <.
h ,  t >.  =  B  ->  ( ( ( A  .~  <. h ,  t >.  /\  <. h ,  t >.  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )  <->  ( ( A  .~  B  /\  B  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )
) )
19 breq2 4027 . . . . 5  |-  ( <.
s ,  r >.  =  C  ->  ( B  .~  <. s ,  r
>. 
<->  B  .~  C ) )
2019anbi2d 684 . . . 4  |-  ( <.
s ,  r >.  =  C  ->  ( ( A  .~  B  /\  B  .~  <. s ,  r
>. )  <->  ( A  .~  B  /\  B  .~  C
) ) )
21 breq2 4027 . . . 4  |-  ( <.
s ,  r >.  =  C  ->  ( A  .~  <. s ,  r
>. 
<->  A  .~  C ) )
2220, 21imbi12d 311 . . 3  |-  ( <.
s ,  r >.  =  C  ->  ( ( ( A  .~  B  /\  B  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )  <->  ( ( A  .~  B  /\  B  .~  C )  ->  A  .~  C
) ) )
231ecopoveq 6759 . . . . . . . 8  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S ) )  -> 
( <. f ,  g
>.  .~  <. h ,  t
>. 
<->  ( f  .+  t
)  =  ( g 
.+  h ) ) )
24233adant3 975 . . . . . . 7  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( <. f ,  g >.  .~  <. h ,  t >.  <->  ( f  .+  t )  =  ( g  .+  h ) ) )
251ecopoveq 6759 . . . . . . . 8  |-  ( ( ( h  e.  S  /\  t  e.  S
)  /\  ( s  e.  S  /\  r  e.  S ) )  -> 
( <. h ,  t
>.  .~  <. s ,  r
>. 
<->  ( h  .+  r
)  =  ( t 
.+  s ) ) )
26253adant1 973 . . . . . . 7  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( <. h ,  t >.  .~  <. s ,  r >.  <->  ( h  .+  r )  =  ( t  .+  s ) ) )
2724, 26anbi12d 691 . . . . . 6  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( ( <. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  <->  ( ( f 
.+  t )  =  ( g  .+  h
)  /\  ( h  .+  r )  =  ( t  .+  s ) ) ) )
28 oveq12 5867 . . . . . . 7  |-  ( ( ( f  .+  t
)  =  ( g 
.+  h )  /\  ( h  .+  r )  =  ( t  .+  s ) )  -> 
( ( f  .+  t )  .+  (
h  .+  r )
)  =  ( ( g  .+  h ) 
.+  ( t  .+  s ) ) )
29 vex 2791 . . . . . . . 8  |-  h  e. 
_V
30 vex 2791 . . . . . . . 8  |-  t  e. 
_V
31 vex 2791 . . . . . . . 8  |-  f  e. 
_V
32 ecopopr.com . . . . . . . 8  |-  ( x 
.+  y )  =  ( y  .+  x
)
33 ecopopr.ass . . . . . . . 8  |-  ( ( x  .+  y ) 
.+  z )  =  ( x  .+  (
y  .+  z )
)
34 vex 2791 . . . . . . . 8  |-  r  e. 
_V
3529, 30, 31, 32, 33, 34caov411 6052 . . . . . . 7  |-  ( ( h  .+  t ) 
.+  ( f  .+  r ) )  =  ( ( f  .+  t )  .+  (
h  .+  r )
)
36 vex 2791 . . . . . . . . 9  |-  g  e. 
_V
37 vex 2791 . . . . . . . . 9  |-  s  e. 
_V
3836, 30, 29, 32, 33, 37caov411 6052 . . . . . . . 8  |-  ( ( g  .+  t ) 
.+  ( h  .+  s ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)
3936, 30, 29, 32, 33, 37caov4 6051 . . . . . . . 8  |-  ( ( g  .+  t ) 
.+  ( h  .+  s ) )  =  ( ( g  .+  h )  .+  (
t  .+  s )
)
4038, 39eqtr3i 2305 . . . . . . 7  |-  ( ( h  .+  t ) 
.+  ( g  .+  s ) )  =  ( ( g  .+  h )  .+  (
t  .+  s )
)
4128, 35, 403eqtr4g 2340 . . . . . 6  |-  ( ( ( f  .+  t
)  =  ( g 
.+  h )  /\  ( h  .+  r )  =  ( t  .+  s ) )  -> 
( ( h  .+  t )  .+  (
f  .+  r )
)  =  ( ( h  .+  t ) 
.+  ( g  .+  s ) ) )
4227, 41syl6bi 219 . . . . 5  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( ( <. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  ->  ( ( h  .+  t ) 
.+  ( f  .+  r ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
) ) )
43 ecopopr.cl . . . . . . . . . . 11  |-  ( ( x  e.  S  /\  y  e.  S )  ->  ( x  .+  y
)  e.  S )
4443caovcl 6014 . . . . . . . . . 10  |-  ( ( h  e.  S  /\  t  e.  S )  ->  ( h  .+  t
)  e.  S )
4543caovcl 6014 . . . . . . . . . 10  |-  ( ( f  e.  S  /\  r  e.  S )  ->  ( f  .+  r
)  e.  S )
46 ovex 5883 . . . . . . . . . . 11  |-  ( g 
.+  s )  e. 
_V
47 ecopopr.can . . . . . . . . . . 11  |-  ( ( x  e.  S  /\  y  e.  S )  ->  ( ( x  .+  y )  =  ( x  .+  z )  ->  y  =  z ) )
4846, 47caovcan 6024 . . . . . . . . . 10  |-  ( ( ( h  .+  t
)  e.  S  /\  ( f  .+  r
)  e.  S )  ->  ( ( ( h  .+  t ) 
.+  ( f  .+  r ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)  ->  ( f  .+  r )  =  ( g  .+  s ) ) )
4944, 45, 48syl2an 463 . . . . . . . . 9  |-  ( ( ( h  e.  S  /\  t  e.  S
)  /\  ( f  e.  S  /\  r  e.  S ) )  -> 
( ( ( h 
.+  t )  .+  ( f  .+  r
) )  =  ( ( h  .+  t
)  .+  ( g  .+  s ) )  -> 
( f  .+  r
)  =  ( g 
.+  s ) ) )
50493impb 1147 . . . . . . . 8  |-  ( ( ( h  e.  S  /\  t  e.  S
)  /\  f  e.  S  /\  r  e.  S
)  ->  ( (
( h  .+  t
)  .+  ( f  .+  r ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)  ->  ( f  .+  r )  =  ( g  .+  s ) ) )
51503com12 1155 . . . . . . 7  |-  ( ( f  e.  S  /\  ( h  e.  S  /\  t  e.  S
)  /\  r  e.  S )  ->  (
( ( h  .+  t )  .+  (
f  .+  r )
)  =  ( ( h  .+  t ) 
.+  ( g  .+  s ) )  -> 
( f  .+  r
)  =  ( g 
.+  s ) ) )
52513adant3l 1178 . . . . . 6  |-  ( ( f  e.  S  /\  ( h  e.  S  /\  t  e.  S
)  /\  ( s  e.  S  /\  r  e.  S ) )  -> 
( ( ( h 
.+  t )  .+  ( f  .+  r
) )  =  ( ( h  .+  t
)  .+  ( g  .+  s ) )  -> 
( f  .+  r
)  =  ( g 
.+  s ) ) )
53523adant1r 1175 . . . . 5  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( (
( h  .+  t
)  .+  ( f  .+  r ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)  ->  ( f  .+  r )  =  ( g  .+  s ) ) )
5442, 53syld 40 . . . 4  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( ( <. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  ->  ( f 
.+  r )  =  ( g  .+  s
) ) )
551ecopoveq 6759 . . . . 5  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( s  e.  S  /\  r  e.  S ) )  -> 
( <. f ,  g
>.  .~  <. s ,  r
>. 
<->  ( f  .+  r
)  =  ( g 
.+  s ) ) )
56553adant2 974 . . . 4  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( <. f ,  g >.  .~  <. s ,  r >.  <->  ( f  .+  r )  =  ( g  .+  s ) ) )
5754, 56sylibrd 225 . . 3  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S )  /\  (
s  e.  S  /\  r  e.  S )
)  ->  ( ( <. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  ->  <. f ,  g >.  .~  <. s ,  r >. )
)
5810, 14, 18, 22, 573optocl 4766 . 2  |-  ( ( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S
) )  ->  (
( A  .~  B  /\  B  .~  C )  ->  A  .~  C
) )
599, 58mpcom 32 1  |-  ( ( A  .~  B  /\  B  .~  C )  ->  A  .~  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   E.wex 1528    = wceq 1623    e. wcel 1684   <.cop 3643   class class class wbr 4023   {copab 4076    X. cxp 4687  (class class class)co 5858
This theorem is referenced by:  ecopover  6762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator