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	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}$$
	ecopopr.com	$$⊢x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
Assertion	ecopovsym	$$⊢A\underset{\dot{}}{\sim }B\to B\underset{\dot{}}{\sim }A$$

Proof

Step	Hyp	Ref	Expression
1		ecopopr.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}$$
2		ecopopr.com	$$⊢x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x$$
3		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in \left(S\times S\right)\wedge y\in \left(S\times S\right)\right)\wedge \exists z\exists w\exists v\exists u\left(\left(x=⟨z,w⟩\wedge y=⟨v,u⟩\right)\wedge z\underset{\dot{}}{+}u=w\underset{\dot{}}{+}v\right)\right)\right\}\subseteq \left(S\times S\right)\times \left(S\times S\right)$$
4	1 3	eqsstri	$$⊢\underset{\dot{}}{\sim }\subseteq \left(S\times S\right)\times \left(S\times S\right)$$
5	4	brel	$$⊢A\underset{\dot{}}{\sim }B\to \left(A\in \left(S\times S\right)\wedge B\in \left(S\times S\right)\right)$$
6		eqid	$$⊢S\times S=S\times S$$
7		breq1	$$⊢⟨f,g⟩=A\to \left(⟨f,g⟩\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow A\underset{\dot{}}{\sim }⟨h,t⟩\right)$$
8		breq2	$$⊢⟨f,g⟩=A\to \left(⟨h,t⟩\underset{\dot{}}{\sim }⟨f,g⟩\leftrightarrow ⟨h,t⟩\underset{\dot{}}{\sim }A\right)$$
9	7 8	bibi12d	$$⊢⟨f,g⟩=A\to \left(\left(⟨f,g⟩\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow ⟨h,t⟩\underset{\dot{}}{\sim }⟨f,g⟩\right)\leftrightarrow \left(A\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow ⟨h,t⟩\underset{\dot{}}{\sim }A\right)\right)$$
10		breq2	$$⊢⟨h,t⟩=B\to \left(A\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow A\underset{\dot{}}{\sim }B\right)$$
11		breq1	$$⊢⟨h,t⟩=B\to \left(⟨h,t⟩\underset{\dot{}}{\sim }A\leftrightarrow B\underset{\dot{}}{\sim }A\right)$$
12	10 11	bibi12d	$$⊢⟨h,t⟩=B\to \left(\left(A\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow ⟨h,t⟩\underset{\dot{}}{\sim }A\right)\leftrightarrow \left(A\underset{\dot{}}{\sim }B\leftrightarrow B\underset{\dot{}}{\sim }A\right)\right)$$
13	1	ecopoveq	$$⊢\left(\left(f\in S\wedge g\in S\right)\wedge \left(h\in S\wedge t\in S\right)\right)\to \left(⟨f,g⟩\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow f\underset{\dot{}}{+}t=g\underset{\dot{}}{+}h\right)$$
14		vex	$$⊢f\in \mathrm{V}$$
15		vex	$$⊢t\in \mathrm{V}$$
16	14 15 2	caovcom	$$⊢f\underset{\dot{}}{+}t=t\underset{\dot{}}{+}f$$
17		vex	$$⊢g\in \mathrm{V}$$
18		vex	$$⊢h\in \mathrm{V}$$
19	17 18 2	caovcom	$$⊢g\underset{\dot{}}{+}h=h\underset{\dot{}}{+}g$$
20	16 19	eqeq12i	$$⊢f\underset{\dot{}}{+}t=g\underset{\dot{}}{+}h\leftrightarrow t\underset{\dot{}}{+}f=h\underset{\dot{}}{+}g$$
21		eqcom	$$⊢t\underset{\dot{}}{+}f=h\underset{\dot{}}{+}g\leftrightarrow h\underset{\dot{}}{+}g=t\underset{\dot{}}{+}f$$
22	20 21	bitri	$$⊢f\underset{\dot{}}{+}t=g\underset{\dot{}}{+}h\leftrightarrow h\underset{\dot{}}{+}g=t\underset{\dot{}}{+}f$$
23	13 22	bitrdi	$$⊢\left(\left(f\in S\wedge g\in S\right)\wedge \left(h\in S\wedge t\in S\right)\right)\to \left(⟨f,g⟩\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow h\underset{\dot{}}{+}g=t\underset{\dot{}}{+}f\right)$$
24	1	ecopoveq	$$⊢\left(\left(h\in S\wedge t\in S\right)\wedge \left(f\in S\wedge g\in S\right)\right)\to \left(⟨h,t⟩\underset{\dot{}}{\sim }⟨f,g⟩\leftrightarrow h\underset{\dot{}}{+}g=t\underset{\dot{}}{+}f\right)$$
25	24	ancoms	$$⊢\left(\left(f\in S\wedge g\in S\right)\wedge \left(h\in S\wedge t\in S\right)\right)\to \left(⟨h,t⟩\underset{\dot{}}{\sim }⟨f,g⟩\leftrightarrow h\underset{\dot{}}{+}g=t\underset{\dot{}}{+}f\right)$$
26	23 25	bitr4d	$$⊢\left(\left(f\in S\wedge g\in S\right)\wedge \left(h\in S\wedge t\in S\right)\right)\to \left(⟨f,g⟩\underset{\dot{}}{\sim }⟨h,t⟩\leftrightarrow ⟨h,t⟩\underset{\dot{}}{\sim }⟨f,g⟩\right)$$
27	6 9 12 26	2optocl	$$⊢\left(A\in \left(S\times S\right)\wedge B\in \left(S\times S\right)\right)\to \left(A\underset{\dot{}}{\sim }B\leftrightarrow B\underset{\dot{}}{\sim }A\right)$$
28	5 27	syl	$$⊢A\underset{\dot{}}{\sim }B\to \left(A\underset{\dot{}}{\sim }B\leftrightarrow B\underset{\dot{}}{\sim }A\right)$$
29	28	ibi	$$⊢A\underset{\dot{}}{\sim }B\to B\underset{\dot{}}{\sim }A$$