Metamath Proof Explorer


Theorem ecopover

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 an equivalence relation. (Contributed by NM, 16-Feb-1996) (Revised by Mario Carneiro, 12-Aug-2015) (Proof shortened by AV, 1-May-2021)

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 ecopover
|- .~ Er ( S X. S )

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 1 relopabiv
 |-  Rel .~
7 1 2 ecopovsym
 |-  ( f .~ g -> g .~ f )
8 1 2 3 4 5 ecopovtrn
 |-  ( ( f .~ g /\ g .~ h ) -> f .~ h )
9 vex
 |-  g e. _V
10 vex
 |-  h e. _V
11 9 10 2 caovcom
 |-  ( g .+ h ) = ( h .+ g )
12 1 ecopoveq
 |-  ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> ( <. g , h >. .~ <. g , h >. <-> ( g .+ h ) = ( h .+ g ) ) )
13 11 12 mpbiri
 |-  ( ( ( g e. S /\ h e. S ) /\ ( g e. S /\ h e. S ) ) -> <. g , h >. .~ <. g , h >. )
14 13 anidms
 |-  ( ( g e. S /\ h e. S ) -> <. g , h >. .~ <. g , h >. )
15 14 rgen2
 |-  A. g e. S A. h e. S <. g , h >. .~ <. g , h >.
16 breq12
 |-  ( ( f = <. g , h >. /\ f = <. g , h >. ) -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
17 16 anidms
 |-  ( f = <. g , h >. -> ( f .~ f <-> <. g , h >. .~ <. g , h >. ) )
18 17 ralxp
 |-  ( A. f e. ( S X. S ) f .~ f <-> A. g e. S A. h e. S <. g , h >. .~ <. g , h >. )
19 15 18 mpbir
 |-  A. f e. ( S X. S ) f .~ f
20 19 rspec
 |-  ( f e. ( S X. S ) -> f .~ f )
21 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 ) )
22 1 21 eqsstri
 |-  .~ C_ ( ( S X. S ) X. ( S X. S ) )
23 22 ssbri
 |-  ( f .~ f -> f ( ( S X. S ) X. ( S X. S ) ) f )
24 brxp
 |-  ( f ( ( S X. S ) X. ( S X. S ) ) f <-> ( f e. ( S X. S ) /\ f e. ( S X. S ) ) )
25 24 simplbi
 |-  ( f ( ( S X. S ) X. ( S X. S ) ) f -> f e. ( S X. S ) )
26 23 25 syl
 |-  ( f .~ f -> f e. ( S X. S ) )
27 20 26 impbii
 |-  ( f e. ( S X. S ) <-> f .~ f )
28 6 7 8 27 iseri
 |-  .~ Er ( S X. S )