# Metamath Proof Explorer

Description: Lemma for paddass . The case when p = z . (Contributed by NM, 11-Jan-2012)

Ref Expression
`|- .<_ = ( le ` K )`
`|- .\/ = ( join ` K )`
`|- A = ( Atoms ` K )`
`|- .+ = ( +P ` K )`
`|- ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> p e. ( ( X .+ Y ) .+ Z ) )`

### Proof

Step Hyp Ref Expression
` |-  .<_ = ( le ` K )`
` |-  .\/ = ( join ` K )`
` |-  A = ( Atoms ` K )`
` |-  .+ = ( +P ` K )`
5 simplll
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> K e. HL )`
6 simplr3
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> Z C_ A )`
7 simplr1
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> X C_ A )`
8 simplr2
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> Y C_ A )`
` |-  ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) C_ A )`
10 5 7 8 9 syl3anc
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> ( X .+ Y ) C_ A )`
` |-  ( ( K e. HL /\ Z C_ A /\ ( X .+ Y ) C_ A ) -> Z C_ ( ( X .+ Y ) .+ Z ) )`
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> Z C_ ( ( X .+ Y ) .+ Z ) )`
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> p = z )`
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> z e. Z )`
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> p e. Z )`
` |-  ( ( ( ( K e. HL /\ p = z ) /\ ( X C_ A /\ Y C_ A /\ Z C_ A ) ) /\ z e. Z ) -> p e. ( ( X .+ Y ) .+ Z ) )`