Theorem ecovidi 6154

Description: Lemma used to transfer a distributive law via an equivalence relation. (Contributed by Jim Kingdon, 17-Sep-2019.)

Hypotheses

Ref	Expression
ecovidi.1	⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )
ecovidi.2	⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )
ecovidi.3	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )
ecovidi.4	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )
ecovidi.5	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )
ecovidi.6	⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )
ecovidi.7	⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))
ecovidi.8	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))
ecovidi.9	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))
ecovidi.10	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐻 = 𝐾)
ecovidi.11	⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐽 = 𝐿)

Assertion

Ref	Expression
ecovidi	⊢ ((A ∈ 𝐷 ∧ B ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

Distinct variable groups:   x,y,z,w,v,u,A   z,B,w,v,u   w,𝐶,v,u   x, + ,y,z,w,v,u   x, ∼ ,y,z,w,v,u   x,𝑆,y,z,w,v,u   x, · ,y,z,w,v,u   z,𝐷,w,v,u

Allowed substitution hints:   B(x,y)   𝐶(x,y,z)   𝐷(x,y)   𝐻(x,y,z,w,v,u)   𝐽(x,y,z,w,v,u)   𝐾(x,y,z,w,v,u)   𝐿(x,y,z,w,v,u)   𝑀(x,y,z,w,v,u)   𝑁(x,y,z,w,v,u)   𝑊(x,y,z,w,v,u)   𝑋(x,y,z,w,v,u)   𝑌(x,y,z,w,v,u)   𝑍(x,y,z,w,v,u)

Proof of Theorem ecovidi

Step	Hyp	Ref	Expression
1		ecovidi.1	. 2 ⊢ 𝐷 = ((𝑆 × 𝑆) / ∼ )
2		oveq1 5462	. . 3 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )))
3		oveq1 5462	. . . 4 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) = (A · [⟨z, w⟩] ∼ ))
4		oveq1 5462	. . . 4 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ ) = (A · [⟨v, u⟩] ∼ ))
5	3, 4	oveq12d 5473	. . 3 ⊢ ([⟨x, y⟩] ∼ = A → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ )))
6	2, 5	eqeq12d 2051	. 2 ⊢ ([⟨x, y⟩] ∼ = A → (([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) ↔ (A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ ))))
7		oveq1 5462	. . . 4 ⊢ ([⟨z, w⟩] ∼ = B → ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ ) = (B + [⟨v, u⟩] ∼ ))
8	7	oveq2d 5471	. . 3 ⊢ ([⟨z, w⟩] ∼ = B → (A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (A · (B + [⟨v, u⟩] ∼ )))
9		oveq2 5463	. . . 4 ⊢ ([⟨z, w⟩] ∼ = B → (A · [⟨z, w⟩] ∼ ) = (A · B))
10	9	oveq1d 5470	. . 3 ⊢ ([⟨z, w⟩] ∼ = B → ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ )) = ((A · B) + (A · [⟨v, u⟩] ∼ )))
11	8, 10	eqeq12d 2051	. 2 ⊢ ([⟨z, w⟩] ∼ = B → ((A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ )) ↔ (A · (B + [⟨v, u⟩] ∼ )) = ((A · B) + (A · [⟨v, u⟩] ∼ ))))
12		oveq2 5463	. . . 4 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (B + [⟨v, u⟩] ∼ ) = (B + 𝐶))
13	12	oveq2d 5471	. . 3 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (A · (B + [⟨v, u⟩] ∼ )) = (A · (B + 𝐶)))
14		oveq2 5463	. . . 4 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (A · [⟨v, u⟩] ∼ ) = (A · 𝐶))
15	14	oveq2d 5471	. . 3 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → ((A · B) + (A · [⟨v, u⟩] ∼ )) = ((A · B) + (A · 𝐶)))
16	13, 15	eqeq12d 2051	. 2 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → ((A · (B + [⟨v, u⟩] ∼ )) = ((A · B) + (A · [⟨v, u⟩] ∼ )) ↔ (A · (B + 𝐶)) = ((A · B) + (A · 𝐶))))
17		ecovidi.10	. . . 4 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐻 = 𝐾)
18		ecovidi.11	. . . 4 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → 𝐽 = 𝐿)
19		opeq12 3542	. . . . 5 ⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → ⟨𝐻, 𝐽⟩ = ⟨𝐾, 𝐿⟩)
20	19	eceq1d 6078	. . . 4 ⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → [⟨𝐻, 𝐽⟩] ∼ = [⟨𝐾, 𝐿⟩] ∼ )
21	17, 18, 20	syl2anc 391	. . 3 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → [⟨𝐻, 𝐽⟩] ∼ = [⟨𝐾, 𝐿⟩] ∼ )
22		ecovidi.2	. . . . . . 7 ⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )
23	22	oveq2d 5471	. . . . . 6 ⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = ([⟨x, y⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ))
24	23	adantl 262	. . . . 5 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = ([⟨x, y⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ))
25		ecovidi.7	. . . . . 6 ⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆))
26		ecovidi.3	. . . . . 6 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (𝑀 ∈ 𝑆 ∧ 𝑁 ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )
27	25, 26	sylan2 270	. . . . 5 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([⟨x, y⟩] ∼ · [⟨𝑀, 𝑁⟩] ∼ ) = [⟨𝐻, 𝐽⟩] ∼ )
28	24, 27	eqtrd 2069	. . . 4 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = [⟨𝐻, 𝐽⟩] ∼ )
29	28	3impb 1099	. . 3 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = [⟨𝐻, 𝐽⟩] ∼ )
30		ecovidi.4	. . . . . 6 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) = [⟨𝑊, 𝑋⟩] ∼ )
31		ecovidi.5	. . . . . 6 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ ) = [⟨𝑌, 𝑍⟩] ∼ )
32	30, 31	oveqan12d 5474	. . . . 5 ⊢ ((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ))
33		ecovidi.8	. . . . . 6 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) → (𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆))
34		ecovidi.9	. . . . . 6 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆))
35		ecovidi.6	. . . . . 6 ⊢ (((𝑊 ∈ 𝑆 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆)) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )
36	33, 34, 35	syl2an 273	. . . . 5 ⊢ ((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([⟨𝑊, 𝑋⟩] ∼ + [⟨𝑌, 𝑍⟩] ∼ ) = [⟨𝐾, 𝐿⟩] ∼ )
37	32, 36	eqtrd 2069	. . . 4 ⊢ ((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = [⟨𝐾, 𝐿⟩] ∼ )
38	37	3impdi 1189	. . 3 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = [⟨𝐾, 𝐿⟩] ∼ )
39	21, 29, 38	3eqtr4d 2079	. 2 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )))
40	1, 6, 11, 16, 39	3ecoptocl 6131	1 ⊢ ((A ∈ 𝐷 ∧ B ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ⟨cop 3370   × cxp 4286  (class class class)co 5455  [cec 6040   / cqs 6041

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-xp 4294  df-cnv 4296  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fv 4853  df-ov 5458  df-ec 6044  df-qs 6048

This theorem is referenced by:  distrnqg  6371  distrsrg  6647  axdistr  6718