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 ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ 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 ∈ 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 ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B
17 5 11 14 16 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ X join ⁡ K oc ⁡ 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 ⁡ X join ⁡ K oc ⁡ K ⁡ Y ∈ B ∧ Z ∈ 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 ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ 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 ∈ 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 ⁡ 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 ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ 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 ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ 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 ∈ OL ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y = X ∧ ˙ Y
27 26 3adant3r3 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ K ⁡ Y = X ∧ ˙ Y
28 27 oveq1d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X join ⁡ K oc ⁡ 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 ⁡ X join ⁡ K oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z
30 1 15 latjcl ⊢ K ∈ Lat ∧ oc ⁡ K ⁡ Y ∈ B ∧ oc ⁡ K ⁡ Z ∈ B → oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z ∈ B
31 5 14 22 30 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z ∈ B
32 1 15 2 9 oldmj2 ⊢ K ∈ OL ∧ X ∈ B ∧ oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z ∈ 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 ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ 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 ∈ OL ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z = Y ∧ ˙ Z
35 34 3adant3r1 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z = Y ∧ ˙ Z
36 35 oveq2d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ oc ⁡ K ⁡ oc ⁡ K ⁡ Y join ⁡ K oc ⁡ K ⁡ Z = X ∧ ˙ Y ∧ ˙ Z
37 29 33 36 3eqtrd ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = X ∧ ˙ Y ∧ ˙ Z