Metamath Proof Explorer


Theorem qlax5i

Description: One of the equations showing CH is an ortholattice. (This corresponds to axiom "ax-5" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses qlax.1
|- A e. CH
qlax.2
|- B e. CH
Assertion qlax5i
|- ( A vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) = A

Proof

Step Hyp Ref Expression
1 qlax.1
 |-  A e. CH
2 qlax.2
 |-  B e. CH
3 1 2 chdmj2i
 |-  ( _|_ ` ( ( _|_ ` A ) vH B ) ) = ( A i^i ( _|_ ` B ) )
4 3 oveq2i
 |-  ( A vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) = ( A vH ( A i^i ( _|_ ` B ) ) )
5 2 choccli
 |-  ( _|_ ` B ) e. CH
6 1 5 chabs1i
 |-  ( A vH ( A i^i ( _|_ ` B ) ) ) = A
7 4 6 eqtri
 |-  ( A vH ( _|_ ` ( ( _|_ ` A ) vH B ) ) ) = A