ecovdi

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

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

Proof

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

Metamath Proof Explorer

Theorem ecovdi

Proof