Theorem latabs2

Description: Lattice absorption law. From definition of lattice in Kalmbach p. 14. ( chabs2 analog.) (Contributed by NM, 8-Nov-2011)

	Ref	Expression
Hypotheses	latabs1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latabs1.j	⊢ ∨ = ( join ‘ 𝐾 )
	latabs1.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latabs2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		latabs1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latabs1.j	⊢ ∨ = ( join ‘ 𝐾 )
3		latabs1.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5	1 4 2	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) )
6	1 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
7	1 4 3	latleeqm1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 ) )
8	6 7	syld3an3	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑌 ) ↔ ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 ) )
9	5 8	mpbid	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ ( 𝑋 ∨ 𝑌 ) ) = 𝑋 )