This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )