# Metamath Proof Explorer

## Theorem latmassOLD

Description: Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) ( inass analog.) (Contributed by NM, 7-Nov-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses olmass.b
`|- B = ( Base ` K )`
olmass.m
`|- ./\ = ( meet ` K )`
Assertion latmassOLD
`|- ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )`

### Proof

Step Hyp Ref Expression
1 olmass.b
` |-  B = ( Base ` K )`
2 olmass.m
` |-  ./\ = ( meet ` K )`
3 simpl
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OL )`
4 ollat
` |-  ( K e. OL -> K e. Lat )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )`
6 olop
` |-  ( K e. OL -> K e. OP )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. OP )`
8 simpr1
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )`
9 eqid
` |-  ( oc ` K ) = ( oc ` K )`
10 1 9 opoccl
` |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )`
11 7 8 10 syl2anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` X ) e. B )`
12 simpr2
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )`
13 1 9 opoccl
` |-  ( ( K e. OP /\ Y e. B ) -> ( ( oc ` K ) ` Y ) e. B )`
14 7 12 13 syl2anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Y ) e. B )`
15 eqid
` |-  ( join ` K ) = ( join ` K )`
16 1 15 latjcl
` |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B )`
17 5 11 14 16 syl3anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B )`
18 simpr3
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )`
19 1 15 2 9 oldmj3
` |-  ( ( K e. OL /\ ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) )`
20 3 17 18 19 syl3anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) )`
21 1 9 opoccl
` |-  ( ( K e. OP /\ Z e. B ) -> ( ( oc ` K ) ` Z ) e. B )`
22 7 18 21 syl2anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` Z ) e. B )`
23 1 15 latjass
` |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) e. B /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) )`
24 5 11 14 22 23 syl13anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) = ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) )`
25 24 fveq2d
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )`
26 1 15 2 9 oldmj4
` |-  ( ( K e. OL /\ X e. B /\ Y e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X ./\ Y ) )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) = ( X ./\ Y ) )`
28 27 oveq1d
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( oc ` K ) ` Y ) ) ) ./\ Z ) = ( ( X ./\ Y ) ./\ Z ) )`
29 20 25 28 3eqtr3rd
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )`
30 1 15 latjcl
` |-  ( ( K e. Lat /\ ( ( oc ` K ) ` Y ) e. B /\ ( ( oc ` K ) ` Z ) e. B ) -> ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B )`
31 5 14 22 30 syl3anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B )`
32 1 15 2 9 oldmj2
` |-  ( ( K e. OL /\ X e. B /\ ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )`
33 3 8 31 32 syl3anc
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) )`
34 1 15 2 9 oldmj4
` |-  ( ( K e. OL /\ Y e. B /\ Z e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( Y ./\ Z ) )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) = ( Y ./\ Z ) )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X ./\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` Y ) ( join ` K ) ( ( oc ` K ) ` Z ) ) ) ) = ( X ./\ ( Y ./\ Z ) ) )`
` |-  ( ( K e. OL /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )`