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 )