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	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap \left(A{\vee }_{\mathscr{H}}B\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		chub1	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq A{\vee }_{\mathscr{H}}B$$
2		ssid	$$⊢A\subseteq A$$
3	1 2	jctil	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq A\wedge A\subseteq A{\vee }_{\mathscr{H}}B\right)$$
4		ssin	$$⊢\left(A\subseteq A\wedge A\subseteq A{\vee }_{\mathscr{H}}B\right)\leftrightarrow A\subseteq A\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
5	3 4	sylib	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq A\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
6		inss1	$$⊢A\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A$$
7	5 6	jctil	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\wedge A\subseteq A\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
8		eqss	$$⊢A\cap \left(A{\vee }_{\mathscr{H}}B\right)=A\leftrightarrow \left(A\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq A\wedge A\subseteq A\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
9	7 8	sylibr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap \left(A{\vee }_{\mathscr{H}}B\right)=A$$