Theorem latmass

Description: Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	latmass.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latmass.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latmass	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		latmass.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latmass.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		eqid	⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
4	3	odulat	⊢ ( 𝐾 ∈ Lat → ( ODual ‘ 𝐾 ) ∈ Lat )
5	3 1	odubas	⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
6	3 2	odujoin	⊢ ∧ = ( join ‘ ( ODual ‘ 𝐾 ) )
7	5 6	latjass	⊢ ( ( ( ODual ‘ 𝐾 ) ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑍 ) ) )
8	4 7	sylan	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ∧ 𝑌 ) ∧ 𝑍 ) = ( 𝑋 ∧ ( 𝑌 ∧ 𝑍 ) ) )