# Metamath Proof Explorer

## Theorem chabs1

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

Ref Expression
Assertion chabs1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}\left({A}\cap {B}\right)={A}$

### Proof

Step Hyp Ref Expression
1 ssid ${⊢}{A}\subseteq {A}$
2 inss1 ${⊢}{A}\cap {B}\subseteq {A}$
3 1 2 pm3.2i ${⊢}\left({A}\subseteq {A}\wedge {A}\cap {B}\subseteq {A}\right)$
4 simpl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\in {\mathbf{C}}_{ℋ}$
5 chincl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\in {\mathbf{C}}_{ℋ}$
6 chlub ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {A}\wedge {A}\cap {B}\subseteq {A}\right)↔{A}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}\right)$
7 4 5 4 6 syl3anc ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({A}\subseteq {A}\wedge {A}\cap {B}\subseteq {A}\right)↔{A}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}\right)$
8 3 7 mpbii ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}$
9 chub1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {A}{\vee }_{ℋ}\left({A}\cap {B}\right)$
10 5 9 syldan ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {A}{\vee }_{ℋ}\left({A}\cap {B}\right)$
11 8 10 eqssd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}\left({A}\cap {B}\right)={A}$