Metamath Proof Explorer

Theorem paddasslem17

Description: Lemma for paddass . The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012)

Ref Expression
Hypotheses paddass.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
paddass.p ⊢ + = ( +𝑃 ‘ 𝐾 )
Assertion paddasslem17 ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )

Proof

Step Hyp Ref Expression
1 paddass.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 paddass.p ⊢ + = ( +𝑃 ‘ 𝐾 )
3 ianor ⊢ ( ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ↔ ( ¬ ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∨ ¬ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) )
4 ianor ⊢ ( ¬ ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ↔ ( ¬ 𝑋 ≠ ∅ ∨ ¬ ( 𝑌 + 𝑍 ) ≠ ∅ ) )
5 nne ⊢ ( ¬ 𝑋 ≠ ∅ ↔ 𝑋 = ∅ )
6 nne ⊢ ( ¬ ( 𝑌 + 𝑍 ) ≠ ∅ ↔ ( 𝑌 + 𝑍 ) = ∅ )
7 5 6 orbi12i ⊢ ( ( ¬ 𝑋 ≠ ∅ ∨ ¬ ( 𝑌 + 𝑍 ) ≠ ∅ ) ↔ ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) )
8 4 7 bitri ⊢ ( ¬ ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ↔ ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) )
9 ianor ⊢ ( ¬ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ↔ ( ¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅ ) )
10 nne ⊢ ( ¬ 𝑌 ≠ ∅ ↔ 𝑌 = ∅ )
11 nne ⊢ ( ¬ 𝑍 ≠ ∅ ↔ 𝑍 = ∅ )
12 10 11 orbi12i ⊢ ( ( ¬ 𝑌 ≠ ∅ ∨ ¬ 𝑍 ≠ ∅ ) ↔ ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) )
13 9 12 bitri ⊢ ( ¬ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ↔ ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) )
14 8 13 orbi12i ⊢ ( ( ¬ ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∨ ¬ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ↔ ( ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) ∨ ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) ) )
15 3 14 bitri ⊢ ( ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ↔ ( ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) ∨ ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) ) )
16 1 2 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑌 + 𝑍 ) ⊆ 𝐴 )
17 16 3adant3r1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 + 𝑍 ) ⊆ 𝐴 )
18 1 2 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑌 + 𝑍 ) ⊆ 𝐴 ) → ( ∅ + ( 𝑌 + 𝑍 ) ) = ( 𝑌 + 𝑍 ) )
19 17 18 syldan ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ∅ + ( 𝑌 + 𝑍 ) ) = ( 𝑌 + 𝑍 ) )
20 1 2 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( ∅ + 𝑌 ) = 𝑌 )
21 20 3ad2antr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ∅ + 𝑌 ) = 𝑌 )
22 21 oveq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( ∅ + 𝑌 ) + 𝑍 ) = ( 𝑌 + 𝑍 ) )
23 19 22 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ∅ + ( 𝑌 + 𝑍 ) ) = ( ( ∅ + 𝑌 ) + 𝑍 ) )
24 oveq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ∅ + ( 𝑌 + 𝑍 ) ) )
25 oveq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 + 𝑌 ) = ( ∅ + 𝑌 ) )
26 25 oveq1d ⊢ ( 𝑋 = ∅ → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( ∅ + 𝑌 ) + 𝑍 ) )
27 24 26 eqeq12d ⊢ ( 𝑋 = ∅ → ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ↔ ( ∅ + ( 𝑌 + 𝑍 ) ) = ( ( ∅ + 𝑌 ) + 𝑍 ) ) )
28 23 27 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
29 eqimss ⊢ ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
30 28 29 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
31 1 2 padd01 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 + ∅ ) = 𝑋 )
32 31 3ad2antr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ∅ ) = 𝑋 )
33 1 2 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
34 33 3adant3r3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
35 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝐾 ∈ HL )
36 1 2 paddssat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
37 36 3adant3r3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
38 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑍 ⊆ 𝐴 )
39 1 2 sspadd1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
40 35 37 38 39 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
41 34 40 sstrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → 𝑋 ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
42 32 41 eqsstrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ∅ ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
43 oveq2 ⊢ ( ( 𝑌 + 𝑍 ) = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 + ∅ ) )
44 43 sseq1d ⊢ ( ( 𝑌 + 𝑍 ) = ∅ → ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ↔ ( 𝑋 + ∅ ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
45 42 44 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑌 + 𝑍 ) = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
46 30 45 jaod ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
47 1 2 padd02 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑍 ⊆ 𝐴 ) → ( ∅ + 𝑍 ) = 𝑍 )
48 47 3ad2antr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ∅ + 𝑍 ) = 𝑍 )
49 48 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( ∅ + 𝑍 ) ) = ( 𝑋 + 𝑍 ) )
50 32 oveq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + ∅ ) + 𝑍 ) = ( 𝑋 + 𝑍 ) )
51 49 50 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( ∅ + 𝑍 ) ) = ( ( 𝑋 + ∅ ) + 𝑍 ) )
52 oveq1 ⊢ ( 𝑌 = ∅ → ( 𝑌 + 𝑍 ) = ( ∅ + 𝑍 ) )
53 52 oveq2d ⊢ ( 𝑌 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 + ( ∅ + 𝑍 ) ) )
54 oveq2 ⊢ ( 𝑌 = ∅ → ( 𝑋 + 𝑌 ) = ( 𝑋 + ∅ ) )
55 54 oveq1d ⊢ ( 𝑌 = ∅ → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + ∅ ) + 𝑍 ) )
56 53 55 eqeq12d ⊢ ( 𝑌 = ∅ → ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ↔ ( 𝑋 + ( ∅ + 𝑍 ) ) = ( ( 𝑋 + ∅ ) + 𝑍 ) ) )
57 51 56 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
58 1 2 padd01 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑌 + ∅ ) = 𝑌 )
59 58 3ad2antr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑌 + ∅ ) = 𝑌 )
60 59 oveq2d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑌 + ∅ ) ) = ( 𝑋 + 𝑌 ) )
61 1 2 padd01 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → ( ( 𝑋 + 𝑌 ) + ∅ ) = ( 𝑋 + 𝑌 ) )
62 37 61 syldan ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑋 + 𝑌 ) + ∅ ) = ( 𝑋 + 𝑌 ) )
63 60 62 eqtr4d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑋 + ( 𝑌 + ∅ ) ) = ( ( 𝑋 + 𝑌 ) + ∅ ) )
64 oveq2 ⊢ ( 𝑍 = ∅ → ( 𝑌 + 𝑍 ) = ( 𝑌 + ∅ ) )
65 64 oveq2d ⊢ ( 𝑍 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( 𝑋 + ( 𝑌 + ∅ ) ) )
66 oveq2 ⊢ ( 𝑍 = ∅ → ( ( 𝑋 + 𝑌 ) + 𝑍 ) = ( ( 𝑋 + 𝑌 ) + ∅ ) )
67 65 66 eqeq12d ⊢ ( 𝑍 = ∅ → ( ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ↔ ( 𝑋 + ( 𝑌 + ∅ ) ) = ( ( 𝑋 + 𝑌 ) + ∅ ) ) )
68 63 67 syl5ibrcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( 𝑍 = ∅ → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
69 57 68 jaod ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) = ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
70 69 29 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
71 46 70 jaod ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ( ( 𝑋 = ∅ ∨ ( 𝑌 + 𝑍 ) = ∅ ) ∨ ( 𝑌 = ∅ ∨ 𝑍 = ∅ ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
72 15 71 biimtrid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ) → ( ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) )
73 72 3impia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )