# 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}={\mathrm{Base}}_{{K}}$
olmass.m
Assertion latmassOLD

### Proof

Step Hyp Ref Expression
1 olmass.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 olmass.m
3 simpl ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OL}$
4 ollat ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{Lat}$
5 4 adantr ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
6 olop ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{OP}$
7 6 adantr ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OP}$
8 simpr1 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
9 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
10 1 9 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
11 7 8 10 syl2anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
12 simpr2 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
13 1 9 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
14 7 12 13 syl2anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
15 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
16 1 15 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
17 5 11 14 16 syl3anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
18 simpr3 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
19 1 15 2 9 oldmj3
20 3 17 18 19 syl3anc
21 1 9 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Z}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$
22 7 18 21 syl2anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$
23 1 15 latjass ${⊢}\left({K}\in \mathrm{Lat}\wedge \left(\mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}\right)\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\right)$
24 5 11 14 22 23 syl13anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)=\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\right)$
25 24 fveq2d ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left(\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\right)=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{join}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\right)\right)$
26 1 15 2 9 oldmj4
30 1 15 latjcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$
31 5 14 22 30 syl3anc ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\mathrm{join}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Z}\right)\in {B}$