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=BaseK
olmass.m ⊢∧˙=meet⁡K
Assertion latmassOLD ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→X∧˙Y∧˙Z=X∧˙Y∧˙Z

Proof

Step Hyp Ref Expression
1 olmass.b ⊢B=BaseK
2 olmass.m ⊢∧˙=meet⁡K
3 simpl ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→K∈OL
4 ollat ⊢K∈OL→K∈Lat
5 4 adantr ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→K∈Lat
6 olop ⊢K∈OL→K∈OP
7 6 adantr ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→K∈OP
8 simpr1 ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→X∈B
9 eqid ⊢oc⁡K=oc⁡K
10 1 9 opoccl ⊢K∈OP∧X∈B→oc⁡K⁡X∈B
11 7 8 10 syl2anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡X∈B
12 simpr2 ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→Y∈B
13 1 9 opoccl ⊢K∈OP∧Y∈B→oc⁡K⁡Y∈B
14 7 12 13 syl2anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡Y∈B
15 eqid ⊢join⁡K=join⁡K
16 1 15 latjcl ⊢K∈Lat∧oc⁡K⁡X∈B∧oc⁡K⁡Y∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B
17 5 11 14 16 syl3anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B
18 simpr3 ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→Z∈B
19 1 15 2 9 oldmj3 ⊢K∈OL∧oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∧˙Z
20 3 17 18 19 syl3anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∧˙Z
21 1 9 opoccl ⊢K∈OP∧Z∈B→oc⁡K⁡Z∈B
22 7 18 21 syl2anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡Z∈B
23 1 15 latjass ⊢K∈Lat∧oc⁡K⁡X∈B∧oc⁡K⁡Y∈B∧oc⁡K⁡Z∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z
24 5 11 14 22 23 syl13anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z
25 24 fveq2d ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z
26 1 15 2 9 oldmj4 ⊢K∈OL∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y=X∧˙Y
27 26 3adant3r3 ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y=X∧˙Y
28 27 oveq1d ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Y∧˙Z=X∧˙Y∧˙Z
29 20 25 28 3eqtr3rd ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→X∧˙Y∧˙Z=oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z
30 1 15 latjcl ⊢K∈Lat∧oc⁡K⁡Y∈B∧oc⁡K⁡Z∈B→oc⁡K⁡Yjoin⁡Koc⁡K⁡Z∈B
31 5 14 22 30 syl3anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡Yjoin⁡Koc⁡K⁡Z∈B
32 1 15 2 9 oldmj2 ⊢K∈OL∧X∈B∧oc⁡K⁡Yjoin⁡Koc⁡K⁡Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=X∧˙oc⁡K⁡oc⁡K⁡Yjoin⁡Koc⁡K⁡Z
33 3 8 31 32 syl3anc ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Xjoin⁡Koc⁡K⁡Yjoin⁡Koc⁡K⁡Z=X∧˙oc⁡K⁡oc⁡K⁡Yjoin⁡Koc⁡K⁡Z
34 1 15 2 9 oldmj4 ⊢K∈OL∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Yjoin⁡Koc⁡K⁡Z=Y∧˙Z
35 34 3adant3r1 ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→oc⁡K⁡oc⁡K⁡Yjoin⁡Koc⁡K⁡Z=Y∧˙Z
36 35 oveq2d ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→X∧˙oc⁡K⁡oc⁡K⁡Yjoin⁡Koc⁡K⁡Z=X∧˙Y∧˙Z
37 29 33 36 3eqtrd ⊢K∈OL∧X∈B∧Y∈B∧Z∈B→X∧˙Y∧˙Z=X∧˙Y∧˙Z