Theorem olm02

Description: Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012)

	Ref	Expression
Hypotheses	olm0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	olm0.m	⊢ ∧ = ( meet ‘ 𝐾 )
	olm0.z	⊢ 0 = ( 0. ‘ 𝐾 )
Assertion	olm02	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∧ 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		olm0.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		olm0.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		olm0.z	⊢ 0 = ( 0. ‘ 𝐾 )
4		ollat	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ Lat )
5	4	adantr	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
6		simpr	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
7		olop	⊢ ( 𝐾 ∈ OL → 𝐾 ∈ OP )
8	7	adantr	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
9	1 3	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
10	8 9	syl	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → 0 ∈ 𝐵 )
11	1 2	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = ( 0 ∧ 𝑋 ) )
12	5 6 10 11	syl3anc	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = ( 0 ∧ 𝑋 ) )
13	1 2 3	olm01	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∧ 0 ) = 0 )
14	12 13	eqtr3d	⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ) → ( 0 ∧ 𝑋 ) = 0 )