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 ( 𝐴C → ( 𝐴 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 inidm ( 𝐴𝐴 ) = 𝐴
2 1 oveq2i ( 𝐴 ( 𝐴𝐴 ) ) = ( 𝐴 𝐴 )
3 chabs1 ( ( 𝐴C𝐴C ) → ( 𝐴 ( 𝐴𝐴 ) ) = 𝐴 )
4 3 anidms ( 𝐴C → ( 𝐴 ( 𝐴𝐴 ) ) = 𝐴 )
5 2 4 eqtr3id ( 𝐴C → ( 𝐴 𝐴 ) = 𝐴 )