Metamath Proof Explorer

Theorem ecopovtrn

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)

Ref Expression
Hypotheses 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 ecopovtrn 
|- ( ( A .~ B /\ B .~ C ) -> A .~ C )

Proof

Step Hyp Ref Expression
1 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 ) ) ) }
2 ecopopr.com 
 |-  ( x .+ y ) = ( y .+ x )
3 ecopopr.cl 
 |-  ( ( x e. S /\ y e. S ) -> ( x .+ y ) e. S )
4 ecopopr.ass 
 |-  ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) )
5 ecopopr.can 
 |-  ( ( x e. S /\ y e. S ) -> ( ( x .+ y ) = ( x .+ z ) -> y = z ) )
6 opabssxp 
 |-  { <. 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 ) )
7 1 6 eqsstri 
 |-  .~ C_ ( ( S X. S ) X. ( S X. S ) )
8 7 brel 
 |-  ( A .~ B -> ( A e. ( S X. S ) /\ B e. ( S X. S ) ) )
9 8 simpld 
 |-  ( A .~ B -> A e. ( S X. S ) )
10 7 brel 
 |-  ( B .~ C -> ( B e. ( S X. S ) /\ C e. ( S X. S ) ) )
11 9 10 anim12i 
 |-  ( ( A .~ B /\ B .~ C ) -> ( A e. ( S X. S ) /\ ( B e. ( S X. S ) /\ C e. ( S X. S ) ) ) )
12 3anass 
 |-  ( ( 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 ) ) ) )
13 11 12 sylibr 
 |-  ( ( A .~ B /\ B .~ C ) -> ( A e. ( S X. S ) /\ B e. ( S X. S ) /\ C e. ( S X. S ) ) )
14 eqid 
 |-  ( S X. S ) = ( S X. S )
15 breq1 
 |-  ( <. f , g >. = A -> ( <. f , g >. .~ <. h , t >. <-> A .~ <. h , t >. ) )
16 15 anbi1d 
 |-  ( <. f , g >. = A -> ( ( <. f , g >. .~ <. h , t >. /\ <. h , t >. .~ <. s , r >. ) <-> ( A .~ <. h , t >. /\ <. h , t >. .~ <. s , r >. ) ) )
17 breq1 
 |-  ( <. f , g >. = A -> ( <. f , g >. .~ <. s , r >. <-> A .~ <. s , r >. ) )
18 16 17 imbi12d 
 |-  ( <. 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 >. ) ) )
19 breq2 
 |-  ( <. h , t >. = B -> ( A .~ <. h , t >. <-> A .~ B ) )
20 breq1 
 |-  ( <. h , t >. = B -> ( <. h , t >. .~ <. s , r >. <-> B .~ <. s , r >. ) )
21 19 20 anbi12d 
 |-  ( <. h , t >. = B -> ( ( A .~ <. h , t >. /\ <. h , t >. .~ <. s , r >. ) <-> ( A .~ B /\ B .~ <. s , r >. ) ) )
22 21 imbi1d 
 |-  ( <. h , t >. = B -> ( ( ( A .~ <. h , t >. /\ <. h , t >. .~ <. s , r >. ) -> A .~ <. s , r >. ) <-> ( ( A .~ B /\ B .~ <. s , r >. ) -> A .~ <. s , r >. ) ) )
23 breq2 
 |-  ( <. s , r >. = C -> ( B .~ <. s , r >. <-> B .~ C ) )
24 23 anbi2d 
 |-  ( <. s , r >. = C -> ( ( A .~ B /\ B .~ <. s , r >. ) <-> ( A .~ B /\ B .~ C ) ) )
25 breq2 
 |-  ( <. s , r >. = C -> ( A .~ <. s , r >. <-> A .~ C ) )
26 24 25 imbi12d 
 |-  ( <. s , r >. = C -> ( ( ( A .~ B /\ B .~ <. s , r >. ) -> A .~ <. s , r >. ) <-> ( ( A .~ B /\ B .~ C ) -> A .~ C ) ) )
27 1 ecopoveq 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( h e. S /\ t e. S ) ) -> ( <. f , g >. .~ <. h , t >. <-> ( f .+ t ) = ( g .+ h ) ) )
28 27 3adant3 
 |-  ( ( ( 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 ) ) )
29 1 ecopoveq 
 |-  ( ( ( h e. S /\ t e. S ) /\ ( s e. S /\ r e. S ) ) -> ( <. h , t >. .~ <. s , r >. <-> ( h .+ r ) = ( t .+ s ) ) )
30 29 3adant1 
 |-  ( ( ( 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 ) ) )
31 28 30 anbi12d 
 |-  ( ( ( 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 ) ) ) )
32 oveq12 
 |-  ( ( ( f .+ t ) = ( g .+ h ) /\ ( h .+ r ) = ( t .+ s ) ) -> ( ( f .+ t ) .+ ( h .+ r ) ) = ( ( g .+ h ) .+ ( t .+ s ) ) )
33 vex 
 |-  h e. _V
34 vex 
 |-  t e. _V
35 vex 
 |-  f e. _V
36 vex 
 |-  r e. _V
37 33 34 35 2 4 36 caov411 
 |-  ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( f .+ t ) .+ ( h .+ r ) )
38 vex 
 |-  g e. _V
39 vex 
 |-  s e. _V
40 38 34 33 2 4 39 caov411 
 |-  ( ( g .+ t ) .+ ( h .+ s ) ) = ( ( h .+ t ) .+ ( g .+ s ) )
41 38 34 33 2 4 39 caov4 
 |-  ( ( g .+ t ) .+ ( h .+ s ) ) = ( ( g .+ h ) .+ ( t .+ s ) )
42 40 41 eqtr3i 
 |-  ( ( h .+ t ) .+ ( g .+ s ) ) = ( ( g .+ h ) .+ ( t .+ s ) )
43 32 37 42 3eqtr4g 
 |-  ( ( ( f .+ t ) = ( g .+ h ) /\ ( h .+ r ) = ( t .+ s ) ) -> ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( h .+ t ) .+ ( g .+ s ) ) )
44 31 43 syl6bi 
 |-  ( ( ( 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 ) ) ) )
45 3 caovcl 
 |-  ( ( h e. S /\ t e. S ) -> ( h .+ t ) e. S )
46 3 caovcl 
 |-  ( ( f e. S /\ r e. S ) -> ( f .+ r ) e. S )
47 ovex 
 |-  ( g .+ s ) e. _V
48 47 5 caovcan 
 |-  ( ( ( h .+ t ) e. S /\ ( f .+ r ) e. S ) -> ( ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( h .+ t ) .+ ( g .+ s ) ) -> ( f .+ r ) = ( g .+ s ) ) )
49 45 46 48 syl2an 
 |-  ( ( ( h e. S /\ t e. S ) /\ ( f e. S /\ r e. S ) ) -> ( ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( h .+ t ) .+ ( g .+ s ) ) -> ( f .+ r ) = ( g .+ s ) ) )
50 49 3impb 
 |-  ( ( ( h e. S /\ t e. S ) /\ f e. S /\ r e. S ) -> ( ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( h .+ t ) .+ ( g .+ s ) ) -> ( f .+ r ) = ( g .+ s ) ) )
51 50 3com12 
 |-  ( ( f e. S /\ ( h e. S /\ t e. S ) /\ r e. S ) -> ( ( ( h .+ t ) .+ ( f .+ r ) ) = ( ( h .+ t ) .+ ( g .+ s ) ) -> ( f .+ r ) = ( g .+ s ) ) )
52 51 3adant3l 
 |-  ( ( 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 ) ) )
53 52 3adant1r 
 |-  ( ( ( 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 ) ) )
54 44 53 syld 
 |-  ( ( ( 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 ) ) )
55 1 ecopoveq 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( s e. S /\ r e. S ) ) -> ( <. f , g >. .~ <. s , r >. <-> ( f .+ r ) = ( g .+ s ) ) )
56 55 3adant2 
 |-  ( ( ( 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 ) ) )
57 54 56 sylibrd 
 |-  ( ( ( 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 >. ) )
58 14 18 22 26 57 3optocl 
 |-  ( ( A e. ( S X. S ) /\ B e. ( S X. S ) /\ C e. ( S X. S ) ) -> ( ( A .~ B /\ B .~ C ) -> A .~ C ) )
59 13 58 mpcom 
 |-  ( ( A .~ B /\ B .~ C ) -> A .~ C )