This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 ssid ⊢ 𝐴 ⊆ 𝐴
2 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
3 1 2 pm3.2i ⊢ ( 𝐴 ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 )
4 simpl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ∈ Cℋ )
5 chincl ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∩ 𝐵 ) ∈ Cℋ )
6 chlub ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) ↔ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐴 ) )
7 4 5 4 6 syl3anc ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) ↔ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐴 ) )
8 3 7 mpbii ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝐴 )
9 chub1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
10 5 9 syldan ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
11 8 10 eqssd ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐴 )