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 )