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

Proof

Step	Hyp	Ref	Expression
1		ssid	|- A C_ A
2		inss1	|- ( A i^i B ) C_ A
3	1 2	pm3.2i	|- ( A C_ A /\ ( A i^i B ) C_ A )
4		simpl	|- ( ( A e. CH /\ B e. CH ) -> A e. CH )
5		chincl	|- ( ( A e. CH /\ B e. CH ) -> ( A i^i B ) e. CH )
6		chlub	|- ( ( A e. CH /\ ( A i^i B ) e. CH /\ A e. CH ) -> ( ( A C_ A /\ ( A i^i B ) C_ A ) <-> ( A vH ( A i^i B ) ) C_ A ) )
7	4 5 4 6	syl3anc	|- ( ( A e. CH /\ B e. CH ) -> ( ( A C_ A /\ ( A i^i B ) C_ A ) <-> ( A vH ( A i^i B ) ) C_ A ) )
8	3 7	mpbii	|- ( ( A e. CH /\ B e. CH ) -> ( A vH ( A i^i B ) ) C_ A )
9		chub1	|- ( ( A e. CH /\ ( A i^i B ) e. CH ) -> A C_ ( A vH ( A i^i B ) ) )
10	5 9	syldan	|- ( ( A e. CH /\ B e. CH ) -> A C_ ( A vH ( A i^i B ) ) )
11	8 10	eqssd	|- ( ( A e. CH /\ B e. CH ) -> ( A vH ( A i^i B ) ) = A )