Theorem chabs2

Description: Hilbert lattice absorption law. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 16-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chabs2	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		chub1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
2		ssid	⊢ 𝐴 ⊆ 𝐴
3	1 2	jctil	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
4		ssin	⊢ ( ( 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
5	3 4	sylib	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
6		inss1	⊢ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴
7	5 6	jctil	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
8		eqss	⊢ ( ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 ↔ ( ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
9	7 8	sylibr	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 𝐴 )