Metamath Proof Explorer


Theorem chjidm

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

Ref Expression
Assertion chjidm
|- ( A e. CH -> ( A vH A ) = A )

Proof

Step Hyp Ref Expression
1 inidm
 |-  ( A i^i A ) = A
2 1 oveq2i
 |-  ( A vH ( A i^i A ) ) = ( A vH A )
3 chabs1
 |-  ( ( A e. CH /\ A e. CH ) -> ( A vH ( A i^i A ) ) = A )
4 3 anidms
 |-  ( A e. CH -> ( A vH ( A i^i A ) ) = A )
5 2 4 eqtr3id
 |-  ( A e. CH -> ( A vH A ) = A )