Theorem latabs1

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

	Ref	Expression
Hypotheses	latabs1.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latabs1.j	⊢ ∨ = ( join ‘ 𝐾 )
	latabs1.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latabs1	⊢ ( ( 𝐾 ∈ 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 3	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 )
6	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
7	1 4 2	latleeqj2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) )
8	7	3com23	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) )
9	6 8	syld3an3	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑋 ↔ ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 ) )
10	5 9	mpbid	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 )