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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
olmass.m ⊢ ∧ = ( meet ‘ 𝐾 )
Assertion latmassOLD ( ( 𝐾 ∈ OL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑍 ) ) )

Proof

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