Metamath Proof Explorer


Theorem paddasslem18

Description: Lemma for paddass . Combine paddasslem16 and paddasslem17 . (Contributed by NM, 12-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 paddass.a 𝐴 = ( Atoms ‘ 𝐾 )
2 paddass.p + = ( +𝑃𝐾 )
3 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
5 3 4 1 2 paddasslem16 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
6 5 3expa ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) ∧ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
7 1 2 paddasslem17 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ∧ ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
8 7 3expa ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) ∧ ¬ ( ( 𝑋 ≠ ∅ ∧ ( 𝑌 + 𝑍 ) ≠ ∅ ) ∧ ( 𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅ ) ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )
9 6 8 pm2.61dan ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐴𝑌𝐴𝑍𝐴 ) ) → ( 𝑋 + ( 𝑌 + 𝑍 ) ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) )