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 ∧ 𝑋𝑆𝑌𝑆 ) ∧ ( 𝑍𝑆𝑊𝑆 ) ) → ( ( ( 𝑋 + 𝑌 ) + 𝑍 ) ∩ ( ( 𝑋 + 𝑌 ) + 𝑊 ) ) = ( ( 𝑋 + 𝑌 ) + ( ( 𝑋 + 𝑍 ) ∩ ( 𝑌 + 𝑊 ) ) ) )