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

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