Theorem ecovcom

Description: Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995) (Revised by David Abernethy, 4-Jun-2013)

	Ref	Expression
Hypotheses	ecovcom.1	$$⊢C=\left(S\times S\right)/\underset{\dot{}}{\sim }$$
	ecovcom.2	$$⊢\left(\left(x\in S\wedge y\in S\right)\wedge \left(z\in S\wedge w\in S\right)\right)\to \left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨D,G⟩\right]\underset{\dot{}}{\sim }$$
	ecovcom.3	$$⊢\left(\left(z\in S\wedge w\in S\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to \left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=\left[⟨H,J⟩\right]\underset{\dot{}}{\sim }$$
	ecovcom.4	$$⊢D=H$$
	ecovcom.5	$$⊢G=J$$
Assertion	ecovcom	$$⊢\left(A\in C\wedge B\in C\right)\to A\underset{\dot{}}{+}B=B\underset{\dot{}}{+}A$$

Proof

Step	Hyp	Ref	Expression
1		ecovcom.1	$$⊢C=\left(S\times S\right)/\underset{\dot{}}{\sim }$$
2		ecovcom.2	$$⊢\left(\left(x\in S\wedge y\in S\right)\wedge \left(z\in S\wedge w\in S\right)\right)\to \left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨D,G⟩\right]\underset{\dot{}}{\sim }$$
3		ecovcom.3	$$⊢\left(\left(z\in S\wedge w\in S\right)\wedge \left(x\in S\wedge y\in S\right)\right)\to \left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=\left[⟨H,J⟩\right]\underset{\dot{}}{\sim }$$
4		ecovcom.4	$$⊢D=H$$
5		ecovcom.5	$$⊢G=J$$
6		oveq1	$$⊢\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=A\to \left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=A\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }$$
7		oveq2	$$⊢\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=A\to \left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}A$$
8	6 7	eqeq12d	$$⊢\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=A\to \left(\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\leftrightarrow A\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}A\right)$$
9		oveq2	$$⊢\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=B\to A\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=A\underset{\dot{}}{+}B$$
10		oveq1	$$⊢\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=B\to \left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}A=B\underset{\dot{}}{+}A$$
11	9 10	eqeq12d	$$⊢\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=B\to \left(A\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}A\leftrightarrow A\underset{\dot{}}{+}B=B\underset{\dot{}}{+}A\right)$$
12		opeq12	$$⊢\left(D=H\wedge G=J\right)\to ⟨D,G⟩=⟨H,J⟩$$
13	12	eceq1d	$$⊢\left(D=H\wedge G=J\right)\to \left[⟨D,G⟩\right]\underset{\dot{}}{\sim }=\left[⟨H,J⟩\right]\underset{\dot{}}{\sim }$$
14	4 5 13	mp2an	$$⊢\left[⟨D,G⟩\right]\underset{\dot{}}{\sim }=\left[⟨H,J⟩\right]\underset{\dot{}}{\sim }$$
15	3	ancoms	$$⊢\left(\left(x\in S\wedge y\in S\right)\wedge \left(z\in S\wedge w\in S\right)\right)\to \left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }=\left[⟨H,J⟩\right]\underset{\dot{}}{\sim }$$
16	14 2 15	3eqtr4a	$$⊢\left(\left(x\in S\wedge y\in S\right)\wedge \left(z\in S\wedge w\in S\right)\right)\to \left[⟨x,y⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }=\left[⟨z,w⟩\right]\underset{\dot{}}{\sim }\underset{\dot{}}{+}\left[⟨x,y⟩\right]\underset{\dot{}}{\sim }$$
17	1 8 11 16	2ecoptocl	$$⊢\left(A\in C\wedge B\in C\right)\to A\underset{\dot{}}{+}B=B\underset{\dot{}}{+}A$$