ecovass

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

	Ref	Expression
Hypotheses	ecovass.1	$⊢ D = (S \times S) / \underset{˙}{\sim}$
	ecovass.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} = [⟨G, H⟩] \underset{˙}{\sim}$
	ecovass.3	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to [⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨N, Q⟩] \underset{˙}{\sim}$
	ecovass.4	$⊢ ((G \in S \land H \in S) \land (v \in S \land u \in S)) \to [⟨G, H⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨J, K⟩] \underset{˙}{\sim}$
	ecovass.5	$⊢ ((x \in S \land y \in S) \land (N \in S \land Q \in S)) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨N, Q⟩] \underset{˙}{\sim} = [⟨L, M⟩] \underset{˙}{\sim}$
	ecovass.6	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S)) \to (G \in S \land H \in S)$
	ecovass.7	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to (N \in S \land Q \in S)$
	ecovass.8	$⊢ J = L$
	ecovass.9	$⊢ K = M$
Assertion	ecovass	$⊢ (A \in D \land B \in D \land C \in D) \to (A \underset{˙}{+} B) \underset{˙}{+} C = A \underset{˙}{+} (B \underset{˙}{+} C)$

Proof

Step	Hyp	Ref	Expression
1		ecovass.1	$⊢ D = (S \times S) / \underset{˙}{\sim}$
2		ecovass.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} = [⟨G, H⟩] \underset{˙}{\sim}$
3		ecovass.3	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to [⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨N, Q⟩] \underset{˙}{\sim}$
4		ecovass.4	$⊢ ((G \in S \land H \in S) \land (v \in S \land u \in S)) \to [⟨G, H⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨J, K⟩] \underset{˙}{\sim}$
5		ecovass.5	$⊢ ((x \in S \land y \in S) \land (N \in S \land Q \in S)) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨N, Q⟩] \underset{˙}{\sim} = [⟨L, M⟩] \underset{˙}{\sim}$
6		ecovass.6	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S)) \to (G \in S \land H \in S)$
7		ecovass.7	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to (N \in S \land Q \in S)$
8		ecovass.8	$⊢ J = L$
9		ecovass.9	$⊢ K = M$
10		oveq1	$⊢ [⟨x, y⟩] \underset{˙}{\sim} = A \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim} = A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}$
11	10	oveq1d	$⊢ [⟨x, y⟩] \underset{˙}{\sim} = A \to ([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = (A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}$
12		oveq1	$⊢ [⟨x, y⟩] \underset{˙}{\sim} = A \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = A \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim})$
13	11 12	eqeq12d	$⊢ [⟨x, y⟩] \underset{˙}{\sim} = A \to (([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow (A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = A \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}))$
14		oveq2	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = B \to A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim} = A \underset{˙}{+} B$
15	14	oveq1d	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = B \to (A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = (A \underset{˙}{+} B) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}$
16		oveq1	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = B \to [⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}$
17	16	oveq2d	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = B \to A \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = A \underset{˙}{+} (B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim})$
18	15 17	eqeq12d	$⊢ [⟨z, w⟩] \underset{˙}{\sim} = B \to ((A \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = A \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow (A \underset{˙}{+} B) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = A \underset{˙}{+} (B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}))$
19		oveq2	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = C \to (A \underset{˙}{+} B) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = (A \underset{˙}{+} B) \underset{˙}{+} C$
20		oveq2	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = C \to B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = B \underset{˙}{+} C$
21	20	oveq2d	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = C \to A \underset{˙}{+} (B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = A \underset{˙}{+} (B \underset{˙}{+} C)$
22	19 21	eqeq12d	$⊢ [⟨v, u⟩] \underset{˙}{\sim} = C \to ((A \underset{˙}{+} B) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = A \underset{˙}{+} (B \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) \leftrightarrow (A \underset{˙}{+} B) \underset{˙}{+} C = A \underset{˙}{+} (B \underset{˙}{+} C))$
23		opeq12	$⊢ (J = L \land K = M) \to ⟨J, K⟩ = ⟨L, M⟩$
24	23	eceq1d	$⊢ (J = L \land K = M) \to [⟨J, K⟩] \underset{˙}{\sim} = [⟨L, M⟩] \underset{˙}{\sim}$
25	8 9 24	mp2an	$⊢ [⟨J, K⟩] \underset{˙}{\sim} = [⟨L, M⟩] \underset{˙}{\sim}$
26	2	oveq1d	$⊢ ((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}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨G, H⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}$
27	26	adantr	$⊢ (((x \in S \land y \in S) \land (z \in S \land w \in S)) \land (v \in S \land u \in S)) \to ([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨G, H⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}$
28	6 4	sylan	$⊢ (((x \in S \land y \in S) \land (z \in S \land w \in S)) \land (v \in S \land u \in S)) \to [⟨G, H⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨J, K⟩] \underset{˙}{\sim}$
29	27 28	eqtrd	$⊢ (((x \in S \land y \in S) \land (z \in S \land w \in S)) \land (v \in S \land u \in S)) \to ([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨J, K⟩] \underset{˙}{\sim}$
30	29	3impa	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (v \in S \land u \in S)) \to ([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨J, K⟩] \underset{˙}{\sim}$
31	3	oveq2d	$⊢ ((z \in S \land w \in S) \land (v \in S \land u \in S)) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨N, Q⟩] \underset{˙}{\sim}$
32	31	adantl	$⊢ ((x \in S \land y \in S) \land ((z \in S \land w \in S) \land (v \in S \land u \in S))) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨N, Q⟩] \underset{˙}{\sim}$
33	7 5	sylan2	$⊢ ((x \in S \land y \in S) \land ((z \in S \land w \in S) \land (v \in S \land u \in S))) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨N, Q⟩] \underset{˙}{\sim} = [⟨L, M⟩] \underset{˙}{\sim}$
34	32 33	eqtrd	$⊢ ((x \in S \land y \in S) \land ((z \in S \land w \in S) \land (v \in S \land u \in S))) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = [⟨L, M⟩] \underset{˙}{\sim}$
35	34	3impb	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (v \in S \land u \in S)) \to [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim}) = [⟨L, M⟩] \underset{˙}{\sim}$
36	25 30 35	3eqtr4a	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (v \in S \land u \in S)) \to ([⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨z, w⟩] \underset{˙}{\sim}) \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim} = [⟨x, y⟩] \underset{˙}{\sim} \underset{˙}{+} ([⟨z, w⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨v, u⟩] \underset{˙}{\sim})$
37	1 13 18 22 36	3ecoptocl	$⊢ (A \in D \land B \in D \land C \in D) \to (A \underset{˙}{+} B) \underset{˙}{+} C = A \underset{˙}{+} (B \underset{˙}{+} C)$

Metamath Proof Explorer

Theorem ecovass

Proof