Theorem chjidm

Description: Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chjidm	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}A=A$$

Proof

Step	Hyp	Ref	Expression
1		inidm	$$⊢A\cap A=A$$
2	1	oveq2i	$$⊢A{\vee }_{\mathscr{H}}\left(A\cap A\right)=A{\vee }_{\mathscr{H}}A$$
3		chabs1	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}\left(A\cap A\right)=A$$
4	3	anidms	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}\left(A\cap A\right)=A$$
5	2 4	syl5eqr	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to A{\vee }_{\mathscr{H}}A=A$$