Metamath Proof Explorer

Theorem ecopovsym

Description: Assuming the operation F is commutative, show that the relation .~ , specified by the first hypothesis, is symmetric. (Contributed by NM, 27-Aug-1995) (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 )
Assertion ecopovsym 
|- ( A .~ B -> B .~ A )

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 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 ) )
4 1 3 eqsstri 
 |-  .~ C_ ( ( S X. S ) X. ( S X. S ) )
5 4 brel 
 |-  ( A .~ B -> ( A e. ( S X. S ) /\ B e. ( S X. S ) ) )
6 eqid 
 |-  ( S X. S ) = ( S X. S )
7 breq1 
 |-  ( <. f , g >. = A -> ( <. f , g >. .~ <. h , t >. <-> A .~ <. h , t >. ) )
8 breq2 
 |-  ( <. f , g >. = A -> ( <. h , t >. .~ <. f , g >. <-> <. h , t >. .~ A ) )
9 7 8 bibi12d 
 |-  ( <. f , g >. = A -> ( ( <. f , g >. .~ <. h , t >. <-> <. h , t >. .~ <. f , g >. ) <-> ( A .~ <. h , t >. <-> <. h , t >. .~ A ) ) )
10 breq2 
 |-  ( <. h , t >. = B -> ( A .~ <. h , t >. <-> A .~ B ) )
11 breq1 
 |-  ( <. h , t >. = B -> ( <. h , t >. .~ A <-> B .~ A ) )
12 10 11 bibi12d 
 |-  ( <. h , t >. = B -> ( ( A .~ <. h , t >. <-> <. h , t >. .~ A ) <-> ( A .~ B <-> B .~ A ) ) )
13 1 ecopoveq 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( h e. S /\ t e. S ) ) -> ( <. f , g >. .~ <. h , t >. <-> ( f .+ t ) = ( g .+ h ) ) )
14 vex 
 |-  f e. _V
15 vex 
 |-  t e. _V
16 14 15 2 caovcom 
 |-  ( f .+ t ) = ( t .+ f )
17 vex 
 |-  g e. _V
18 vex 
 |-  h e. _V
19 17 18 2 caovcom 
 |-  ( g .+ h ) = ( h .+ g )
20 16 19 eqeq12i 
 |-  ( ( f .+ t ) = ( g .+ h ) <-> ( t .+ f ) = ( h .+ g ) )
21 eqcom 
 |-  ( ( t .+ f ) = ( h .+ g ) <-> ( h .+ g ) = ( t .+ f ) )
22 20 21 bitri 
 |-  ( ( f .+ t ) = ( g .+ h ) <-> ( h .+ g ) = ( t .+ f ) )
23 13 22 bitrdi 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( h e. S /\ t e. S ) ) -> ( <. f , g >. .~ <. h , t >. <-> ( h .+ g ) = ( t .+ f ) ) )
24 1 ecopoveq 
 |-  ( ( ( h e. S /\ t e. S ) /\ ( f e. S /\ g e. S ) ) -> ( <. h , t >. .~ <. f , g >. <-> ( h .+ g ) = ( t .+ f ) ) )
25 24 ancoms 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( h e. S /\ t e. S ) ) -> ( <. h , t >. .~ <. f , g >. <-> ( h .+ g ) = ( t .+ f ) ) )
26 23 25 bitr4d 
 |-  ( ( ( f e. S /\ g e. S ) /\ ( h e. S /\ t e. S ) ) -> ( <. f , g >. .~ <. h , t >. <-> <. h , t >. .~ <. f , g >. ) )
27 6 9 12 26 2optocl 
 |-  ( ( A e. ( S X. S ) /\ B e. ( S X. S ) ) -> ( A .~ B <-> B .~ A ) )
28 5 27 syl 
 |-  ( A .~ B -> ( A .~ B <-> B .~ A ) )
29 28 ibi 
 |-  ( A .~ B -> B .~ A )