Theorem 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	⊢ 𝐷 = ( ( 𝑆 × 𝑆 ) / ∼ )
	ecovdi.2	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ )
	ecovdi.3	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
	ecovdi.4	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ )
	ecovdi.5	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ )
	ecovdi.6	⊢ ( ( ( 𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) ) → ( [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ + [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ ) = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
	ecovdi.7	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) )
	ecovdi.8	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ) )
	ecovdi.9	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) )
	ecovdi.10	⊢ 𝐻 = 𝐾
	ecovdi.11	⊢ 𝐽 = 𝐿
Assertion	ecovdi	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ecovdi.1	⊢ 𝐷 = ( ( 𝑆 × 𝑆 ) / ∼ )
2		ecovdi.2	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ )
3		ecovdi.3	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
4		ecovdi.4	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ )
5		ecovdi.5	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ )
6		ecovdi.6	⊢ ( ( ( 𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) ) → ( [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ + [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ ) = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
7		ecovdi.7	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆 ) )
8		ecovdi.8	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) → ( 𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆 ) )
9		ecovdi.9	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( 𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) )
10		ecovdi.10	⊢ 𝐻 = 𝐾
11		ecovdi.11	⊢ 𝐽 = 𝐿
12		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
13		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) )
14		oveq1	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
15	13 14	oveq12d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
16	12 15	eqeq12d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( 𝐴 · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ) )
17		oveq1	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) )
18	17	oveq2d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( 𝐴 · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 · ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
19		oveq2	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) = ( 𝐴 · 𝐵 ) )
20	19	oveq1d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
21	18 20	eqeq12d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ = 𝐵 → ( ( 𝐴 · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( 𝐴 · ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ) )
22		oveq2	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐵 + 𝐶 ) )
23	22	oveq2d	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( 𝐴 · ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( 𝐴 · ( 𝐵 + 𝐶 ) ) )
24		oveq2	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) = ( 𝐴 · 𝐶 ) )
25	24	oveq2d	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( ( 𝐴 · 𝐵 ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )
26	23 25	eqeq12d	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ = 𝐶 → ( ( 𝐴 · ( 𝐵 + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) ↔ ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) ) )
27		opeq12	⊢ ( ( 𝐻 = 𝐾 ∧ 𝐽 = 𝐿 ) → ⟨ 𝐻 , 𝐽 ⟩ = ⟨ 𝐾 , 𝐿 ⟩ )
28	27	eceq1d	⊢ ( ( 𝐻 = 𝐾 ∧ 𝐽 = 𝐿 ) → [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
29	10 11 28	mp2an	⊢ [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼
30	2	oveq2d	⊢ ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ ) )
31	30	adantl	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ ) )
32	7 3	sylan2	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑀 , 𝑁 ⟩ ] ∼ ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
33	31 32	eqtrd	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
34	33	3impb	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐻 , 𝐽 ⟩ ] ∼ )
35	4 5	oveqan12d	⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ + [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ ) )
36	8 9 6	syl2an	⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( [ ⟨ 𝑊 , 𝑋 ⟩ ] ∼ + [ ⟨ 𝑌 , 𝑍 ⟩ ] ∼ ) = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
37	35 36	eqtrd	⊢ ( ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ) ∧ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
38	37	3impdi	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = [ ⟨ 𝐾 , 𝐿 ⟩ ] ∼ )
39	29 34 38	3eqtr4a	⊢ ( ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆 ) ∧ ( 𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ + [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) = ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑧 , 𝑤 ⟩ ] ∼ ) + ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ∼ · [ ⟨ 𝑣 , 𝑢 ⟩ ] ∼ ) ) )
40	1 16 21 26 39	3ecoptocl	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )