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 S × S y S × S z w v 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 S × S y S × S z w v u x = z w y = v u z + ˙ u = w + ˙ v
2 ecopopr.com x + ˙ y = y + ˙ x
3 opabssxp x y | x S × S y S × S z w v u x = z w y = v u z + ˙ u = w + ˙ v S × S × S × S
4 1 3 eqsstri ˙ S × S × S × S
5 4 brel A ˙ B A S × S B S × S
6 eqid S × S = S × 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 S g S h S t S f g ˙ h t f + ˙ t = g + ˙ h
14 vex f V
15 vex t V
16 14 15 2 caovcom f + ˙ t = t + ˙ f
17 vex g V
18 vex h 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 S g S h S t S f g ˙ h t h + ˙ g = t + ˙ f
24 1 ecopoveq h S t S f S g S h t ˙ f g h + ˙ g = t + ˙ f
25 24 ancoms f S g S h S t S h t ˙ f g h + ˙ g = t + ˙ f
26 23 25 bitr4d f S g S h S t S f g ˙ h t h t ˙ f g
27 6 9 12 26 2optocl A S × S B S × S A ˙ B B ˙ A
28 5 27 syl A ˙ B A ˙ B B ˙ A
29 28 ibi A ˙ B B ˙ A