Theorem ecovidi 6125

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 5439	. . 3 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )))
3		oveq1 5439	. . . 4 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) = (A · [⟨z, w⟩] ∼ ))
4		oveq1 5439	. . . 4 ⊢ ([⟨x, y⟩] ∼ = A → ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ ) = (A · [⟨v, u⟩] ∼ ))
5	3, 4	oveq12d 5450	. . 3 ⊢ ([⟨x, y⟩] ∼ = A → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ )))
6	2, 5	eqeq12d 2032	. 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 5439	. . . 4 ⊢ ([⟨z, w⟩] ∼ = B → ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ ) = (B + [⟨v, u⟩] ∼ ))
8	7	oveq2d 5448	. . 3 ⊢ ([⟨z, w⟩] ∼ = B → (A · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = (A · (B + [⟨v, u⟩] ∼ )))
9		oveq2 5440	. . . 4 ⊢ ([⟨z, w⟩] ∼ = B → (A · [⟨z, w⟩] ∼ ) = (A · B))
10	9	oveq1d 5447	. . 3 ⊢ ([⟨z, w⟩] ∼ = B → ((A · [⟨z, w⟩] ∼ ) + (A · [⟨v, u⟩] ∼ )) = ((A · B) + (A · [⟨v, u⟩] ∼ )))
11	8, 10	eqeq12d 2032	. 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 5440	. . . 4 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (B + [⟨v, u⟩] ∼ ) = (B + 𝐶))
13	12	oveq2d 5448	. . 3 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (A · (B + [⟨v, u⟩] ∼ )) = (A · (B + 𝐶)))
14		oveq2 5440	. . . 4 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → (A · [⟨v, u⟩] ∼ ) = (A · 𝐶))
15	14	oveq2d 5448	. . 3 ⊢ ([⟨v, u⟩] ∼ = 𝐶 → ((A · B) + (A · [⟨v, u⟩] ∼ )) = ((A · B) + (A · 𝐶)))
16	13, 15	eqeq12d 2032	. 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 3521	. . . . 5 ⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → ⟨𝐻, 𝐽⟩ = ⟨𝐾, 𝐿⟩)
20	19	eceq1d 6049	. . . 4 ⊢ ((𝐻 = 𝐾 ∧ 𝐽 = 𝐿) → [⟨𝐻, 𝐽⟩] ∼ = [⟨𝐾, 𝐿⟩] ∼ )
21	17, 18, 20	syl2anc 393	. . 3 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → [⟨𝐻, 𝐽⟩] ∼ = [⟨𝐾, 𝐿⟩] ∼ )
22		ecovidi.2	. . . . . . 7 ⊢ (((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ ) = [⟨𝑀, 𝑁⟩] ∼ )
23	22	oveq2d 5448	. . . . . 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 2050	. . . 4 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ ((z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → ([⟨x, y⟩] ∼ · ([⟨z, w⟩] ∼ + [⟨v, u⟩] ∼ )) = [⟨𝐻, 𝐽⟩] ∼ )
29	28	3impb 1084	. . 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 5451	. . . . 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 2050	. . . 4 ⊢ ((((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆)) ∧ ((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆))) → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = [⟨𝐾, 𝐿⟩] ∼ )
38	37	3impdi 1174	. . 3 ⊢ (((x ∈ 𝑆 ∧ y ∈ 𝑆) ∧ (z ∈ 𝑆 ∧ w ∈ 𝑆) ∧ (v ∈ 𝑆 ∧ u ∈ 𝑆)) → (([⟨x, y⟩] ∼ · [⟨z, w⟩] ∼ ) + ([⟨x, y⟩] ∼ · [⟨v, u⟩] ∼ )) = [⟨𝐾, 𝐿⟩] ∼ )
39	21, 29, 38	3eqtr4d 2060	. 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 6102	1 ⊢ ((A ∈ 𝐷 ∧ B ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) → (A · (B + 𝐶)) = ((A · B) + (A · 𝐶)))

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 871   = wceq 1226   ∈ wcel 1370  ⟨cop 3349   × cxp 4266  (class class class)co 5432  [cec 6011   / cqs 6012

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-xp 4274  df-cnv 4276  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fv 4833  df-ov 5435  df-ec 6015  df-qs 6019

This theorem is referenced by:  distrnqg  6240  distrsrg  6503  axdistr  6567