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

Theorem ecopovtrn 6966
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 4909 . . . . . . 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 3338 . . . . . 6  |-  .~  C_  (
( S  X.  S
)  X.  ( S  X.  S ) )
43brel 4885 . . . . 5  |-  ( A  .~  B  ->  ( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S
) ) )
54simpld 446 . . . 4  |-  ( A  .~  B  ->  A  e.  ( S  X.  S
) )
63brel 4885 . . . 4  |-  ( B  .~  C  ->  ( B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S
) ) )
75, 6anim12i 550 . . 3  |-  ( ( A  .~  B  /\  B  .~  C )  -> 
( A  e.  ( S  X.  S )  /\  ( B  e.  ( S  X.  S
)  /\  C  e.  ( S  X.  S
) ) ) )
8 3anass 940 . . 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 204 . 2  |-  ( ( A  .~  B  /\  B  .~  C )  -> 
( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S ) ) )
10 eqid 2404 . . 3  |-  ( S  X.  S )  =  ( S  X.  S
)
11 breq1 4175 . . . . 5  |-  ( <.
f ,  g >.  =  A  ->  ( <.
f ,  g >.  .~  <. h ,  t
>. 
<->  A  .~  <. h ,  t >. )
)
1211anbi1d 686 . . . 4  |-  ( <.
f ,  g >.  =  A  ->  ( (
<. f ,  g >.  .~  <. h ,  t
>.  /\  <. h ,  t
>.  .~  <. s ,  r
>. )  <->  ( A  .~  <.
h ,  t >.  /\  <. h ,  t
>.  .~  <. s ,  r
>. ) ) )
13 breq1 4175 . . . 4  |-  ( <.
f ,  g >.  =  A  ->  ( <.
f ,  g >.  .~  <. s ,  r
>. 
<->  A  .~  <. s ,  r >. )
)
1412, 13imbi12d 312 . . 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 4176 . . . . 5  |-  ( <.
h ,  t >.  =  B  ->  ( A  .~  <. h ,  t
>. 
<->  A  .~  B ) )
16 breq1 4175 . . . . 5  |-  ( <.
h ,  t >.  =  B  ->  ( <.
h ,  t >.  .~  <. s ,  r
>. 
<->  B  .~  <. s ,  r >. )
)
1715, 16anbi12d 692 . . . 4  |-  ( <.
h ,  t >.  =  B  ->  ( ( A  .~  <. h ,  t >.  /\  <. h ,  t >.  .~  <. s ,  r >. )  <->  ( A  .~  B  /\  B  .~  <. s ,  r
>. ) ) )
1817imbi1d 309 . . 3  |-  ( <.
h ,  t >.  =  B  ->  ( ( ( A  .~  <. h ,  t >.  /\  <. h ,  t >.  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )  <->  ( ( A  .~  B  /\  B  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )
) )
19 breq2 4176 . . . . 5  |-  ( <.
s ,  r >.  =  C  ->  ( B  .~  <. s ,  r
>. 
<->  B  .~  C ) )
2019anbi2d 685 . . . 4  |-  ( <.
s ,  r >.  =  C  ->  ( ( A  .~  B  /\  B  .~  <. s ,  r
>. )  <->  ( A  .~  B  /\  B  .~  C
) ) )
21 breq2 4176 . . . 4  |-  ( <.
s ,  r >.  =  C  ->  ( A  .~  <. s ,  r
>. 
<->  A  .~  C ) )
2220, 21imbi12d 312 . . 3  |-  ( <.
s ,  r >.  =  C  ->  ( ( ( A  .~  B  /\  B  .~  <. s ,  r >. )  ->  A  .~  <. s ,  r >. )  <->  ( ( A  .~  B  /\  B  .~  C )  ->  A  .~  C
) ) )
231ecopoveq 6964 . . . . . . . 8  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( h  e.  S  /\  t  e.  S ) )  -> 
( <. f ,  g
>.  .~  <. h ,  t
>. 
<->  ( f  .+  t
)  =  ( g 
.+  h ) ) )
24233adant3 977 . . . . . . 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 6964 . . . . . . . 8  |-  ( ( ( h  e.  S  /\  t  e.  S
)  /\  ( s  e.  S  /\  r  e.  S ) )  -> 
( <. h ,  t
>.  .~  <. s ,  r
>. 
<->  ( h  .+  r
)  =  ( t 
.+  s ) ) )
26253adant1 975 . . . . . . 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 692 . . . . . 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 6049 . . . . . . 7  |-  ( ( ( f  .+  t
)  =  ( g 
.+  h )  /\  ( h  .+  r )  =  ( t  .+  s ) )  -> 
( ( f  .+  t )  .+  (
h  .+  r )
)  =  ( ( g  .+  h ) 
.+  ( t  .+  s ) ) )
29 vex 2919 . . . . . . . 8  |-  h  e. 
_V
30 vex 2919 . . . . . . . 8  |-  t  e. 
_V
31 vex 2919 . . . . . . . 8  |-  f  e. 
_V
32 ecopopr.com . . . . . . . 8  |-  ( x 
.+  y )  =  ( y  .+  x
)
33 ecopopr.ass . . . . . . . 8  |-  ( ( x  .+  y ) 
.+  z )  =  ( x  .+  (
y  .+  z )
)
34 vex 2919 . . . . . . . 8  |-  r  e. 
_V
3529, 30, 31, 32, 33, 34caov411 6238 . . . . . . 7  |-  ( ( h  .+  t ) 
.+  ( f  .+  r ) )  =  ( ( f  .+  t )  .+  (
h  .+  r )
)
36 vex 2919 . . . . . . . . 9  |-  g  e. 
_V
37 vex 2919 . . . . . . . . 9  |-  s  e. 
_V
3836, 30, 29, 32, 33, 37caov411 6238 . . . . . . . 8  |-  ( ( g  .+  t ) 
.+  ( h  .+  s ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)
3936, 30, 29, 32, 33, 37caov4 6237 . . . . . . . 8  |-  ( ( g  .+  t ) 
.+  ( h  .+  s ) )  =  ( ( g  .+  h )  .+  (
t  .+  s )
)
4038, 39eqtr3i 2426 . . . . . . 7  |-  ( ( h  .+  t ) 
.+  ( g  .+  s ) )  =  ( ( g  .+  h )  .+  (
t  .+  s )
)
4128, 35, 403eqtr4g 2461 . . . . . 6  |-  ( ( ( f  .+  t
)  =  ( g 
.+  h )  /\  ( h  .+  r )  =  ( t  .+  s ) )  -> 
( ( h  .+  t )  .+  (
f  .+  r )
)  =  ( ( h  .+  t ) 
.+  ( g  .+  s ) ) )
4227, 41syl6bi 220 . . . . 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 6200 . . . . . . . . . 10  |-  ( ( h  e.  S  /\  t  e.  S )  ->  ( h  .+  t
)  e.  S )
4543caovcl 6200 . . . . . . . . . 10  |-  ( ( f  e.  S  /\  r  e.  S )  ->  ( f  .+  r
)  e.  S )
46 ovex 6065 . . . . . . . . . . 11  |-  ( g 
.+  s )  e. 
_V
47 ecopopr.can . . . . . . . . . . 11  |-  ( ( x  e.  S  /\  y  e.  S )  ->  ( ( x  .+  y )  =  ( x  .+  z )  ->  y  =  z ) )
4846, 47caovcan 6210 . . . . . . . . . 10  |-  ( ( ( h  .+  t
)  e.  S  /\  ( f  .+  r
)  e.  S )  ->  ( ( ( h  .+  t ) 
.+  ( f  .+  r ) )  =  ( ( h  .+  t )  .+  (
g  .+  s )
)  ->  ( f  .+  r )  =  ( g  .+  s ) ) )
4944, 45, 48syl2an 464 . . . . . . . . 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 1149 . . . . . . . 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 1157 . . . . . . 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 1180 . . . . . 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 1177 . . . . 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 42 . . . 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 6964 . . . . 5  |-  ( ( ( f  e.  S  /\  g  e.  S
)  /\  ( s  e.  S  /\  r  e.  S ) )  -> 
( <. f ,  g
>.  .~  <. s ,  r
>. 
<->  ( f  .+  r
)  =  ( g 
.+  s ) ) )
56553adant2 976 . . . 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 226 . . 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 4913 . 2  |-  ( ( A  e.  ( S  X.  S )  /\  B  e.  ( S  X.  S )  /\  C  e.  ( S  X.  S
) )  ->  (
( A  .~  B  /\  B  .~  C )  ->  A  .~  C
) )
599, 58mpcom 34 1  |-  ( ( A  .~  B  /\  B  .~  C )  ->  A  .~  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1721   <.cop 3777   class class class wbr 4172   {copab 4225    X. cxp 4835  (class class class)co 6040
This theorem is referenced by:  ecopover  6967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-xp 4843  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator