Metamath Proof Explorer

Theorem pmodl42N

Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012) (New usage is discouraged.)

Ref Expression
Hypotheses pmodl42.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
pmodl42.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion pmodl42N ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( ( 𝑋 + 𝑌 ) + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 pmodl42.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2 pmodl42.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 incom ⊢ ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑌 + 𝑊 ) ) = ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
4 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝐾 ∈ HL )
5 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑌 ∈ 𝑆 )
6 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
7 6 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
8 4 5 7 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
9 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑋 ∈ 𝑆 )
10 6 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
11 4 9 10 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
12 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑍 ∈ 𝑆 )
13 6 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆 ) → 𝑍 ⊆ ( Atoms ‘ 𝐾 ) )
14 4 12 13 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑍 ⊆ ( Atoms ‘ 𝐾 ) )
15 6 2 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑍 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) )
16 4 11 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) )
17 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑊 ∈ 𝑆 )
18 1 2 paddclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) → ( 𝑌 + 𝑊 ) ∈ 𝑆 )
19 4 5 17 18 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑌 + 𝑊 ) ∈ 𝑆 )
20 6 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑆 ) → 𝑊 ⊆ ( Atoms ‘ 𝐾 ) )
21 4 17 20 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑊 ⊆ ( Atoms ‘ 𝐾 ) )
22 6 2 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑊 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝑌 ⊆ ( 𝑌 + 𝑊 ) )
23 4 8 21 22 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑌 ⊆ ( 𝑌 + 𝑊 ) )
24 6 1 2 pmod1i ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + 𝑊 ) ∈ 𝑆 ) ) → ( 𝑌 ⊆ ( 𝑌 + 𝑊 ) → ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑌 + 𝑊 ) ) = ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) ) )
25 24 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + 𝑊 ) ∈ 𝑆 ) ∧ 𝑌 ⊆ ( 𝑌 + 𝑊 ) ) → ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑌 + 𝑊 ) ) = ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) )
26 4 8 16 19 23 25 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑌 + 𝑊 ) ) = ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) )
27 3 26 syl5reqr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) = ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) )
28 27 oveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑋 + ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) ) = ( 𝑋 + ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) ) )
29 ssinss1 ⊢ ( ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
30 16 29 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ⊆ ( Atoms ‘ 𝐾 ) )
31 6 2 paddass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ⊆ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑋 + 𝑌 ) + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) = ( 𝑋 + ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) ) )
32 4 11 8 30 31 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) = ( 𝑋 + ( 𝑌 + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) ) )
33 6 2 paddass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑍 ⊆ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
34 4 11 8 14 33 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑋 + ( 𝑌 + 𝑍 ) ) )
35 6 2 padd12N ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑍 ⊆ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
36 4 11 8 14 35 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
37 34 36 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
38 6 2 paddass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑊 ⊆ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑋 + 𝑌 ) + 𝑊 ) = ( 𝑋 + ( 𝑌 + 𝑊 ) ) )
39 4 11 8 21 38 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + 𝑌 ) + 𝑊 ) = ( 𝑋 + ( 𝑌 + 𝑊 ) ) )
40 37 39 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑋 + ( 𝑌 + 𝑊 ) ) ) )
41 incom ⊢ ( ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∩ ( 𝑋 + ( 𝑌 + 𝑊 ) ) ) = ( ( 𝑋 + ( 𝑌 + 𝑊 ) ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
42 40 41 eqtrdi ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( ( 𝑋 + ( 𝑌 + 𝑊 ) ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) )
43 6 1 psubssat ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 + 𝑊 ) ∈ 𝑆 ) → ( 𝑌 + 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) )
44 4 19 43 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑌 + 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) )
45 1 2 paddclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑋 + 𝑍 ) ∈ 𝑆 )
46 4 9 12 45 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑋 + 𝑍 ) ∈ 𝑆 )
47 1 2 paddclN ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑆 ∧ ( 𝑋 + 𝑍 ) ∈ 𝑆 ) → ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∈ 𝑆 )
48 4 5 46 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∈ 𝑆 )
49 6 2 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑍 ⊆ ( Atoms ‘ 𝐾 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑍 ) )
50 4 11 14 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑍 ) )
51 6 2 sspadd2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑍 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ 𝑌 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
52 4 16 8 51 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( 𝑋 + 𝑍 ) ⊆ ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
53 50 52 sstrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → 𝑋 ⊆ ( 𝑌 + ( 𝑋 + 𝑍 ) ) )
54 6 1 2 pmod1i ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∈ 𝑆 ) ) → ( 𝑋 ⊆ ( 𝑌 + ( 𝑋 + 𝑍 ) ) → ( ( 𝑋 + ( 𝑌 + 𝑊 ) ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) = ( 𝑋 + ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) ) ) )
55 54 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + 𝑊 ) ⊆ ( Atoms ‘ 𝐾 ) ∧ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ∈ 𝑆 ) ∧ 𝑋 ⊆ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) → ( ( 𝑋 + ( 𝑌 + 𝑊 ) ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) = ( 𝑋 + ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) ) )
56 4 11 44 48 53 55 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( 𝑋 + ( 𝑌 + 𝑊 ) ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) = ( 𝑋 + ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) ) )
57 42 56 eqtrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( 𝑋 + ( ( 𝑌 + 𝑊 ) ∩ ( 𝑌 + ( 𝑋 + 𝑍 ) ) ) ) )
58 28 32 57 3eqtr4rd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ( 𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( ( 𝑋 + 𝑌 ) + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) )