Theorem chjidm

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

	Ref	Expression
Assertion	chjidm	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∨ℋ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
2	1	oveq2i	⊢ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐴 ) ) = ( 𝐴 ∨ℋ 𝐴 )
3		chabs1	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐴 ) ) = 𝐴 )
4	3	anidms	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐴 ) ) = 𝐴 )
5	2 4	eqtr3id	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ∨ℋ 𝐴 ) = 𝐴 )