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

Metamath Proof Explorer

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 
|- ( ( A e. CH /\ B e. CH ) -> ( A i^i ( A vH B ) ) = A )

Proof

Step Hyp Ref Expression
1 chub1 
 |-  ( ( A e. CH /\ B e. CH ) -> A C_ ( A vH B ) )
2 ssid 
 |-  A C_ A
3 1 2 jctil 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A C_ A /\ A C_ ( A vH B ) ) )
4 ssin 
 |-  ( ( A C_ A /\ A C_ ( A vH B ) ) <-> A C_ ( A i^i ( A vH B ) ) )
5 3 4 sylib 
 |-  ( ( A e. CH /\ B e. CH ) -> A C_ ( A i^i ( A vH B ) ) )
6 inss1 
 |-  ( A i^i ( A vH B ) ) C_ A
7 5 6 jctil 
 |-  ( ( A e. CH /\ B e. CH ) -> ( ( A i^i ( A vH B ) ) C_ A /\ A C_ ( A i^i ( A vH B ) ) ) )
8 eqss 
 |-  ( ( A i^i ( A vH B ) ) = A <-> ( ( A i^i ( A vH B ) ) C_ A /\ A C_ ( A i^i ( A vH B ) ) ) )
9 7 8 sylibr 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A i^i ( A vH B ) ) = A )