This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (S \times S) / \underset{˙}{\sim}$
		ecovcom.2	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S)) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim} = [⟨D, G⟩] \underset{˙}{\sim}$
		ecovcom.3	$⊢ ((z \in S \land w \in S) \land (x \in S \land y \in S)) \to [⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨x, y⟩] \underset{˙}{\sim} = [⟨H, J⟩] \underset{˙}{\sim}$
		ecovcom.4	$⊢ D = H$
		ecovcom.5	$⊢ G = J$
	Assertion	ecovcom	$⊢ (A \in C \land B \in C) \to A \underset{˙}{+} B = B \underset{˙}{+} A$

Proof

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