Metamath Proof Explorer


Theorem pjoml5i

Description: The orthomodular law. Remark in Kalmbach p. 22. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1
|- A e. CH
pjoml2.2
|- B e. CH
Assertion pjoml5i
|- ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B )

Proof

Step Hyp Ref Expression
1 pjoml2.1
 |-  A e. CH
2 pjoml2.2
 |-  B e. CH
3 1 2 chub1i
 |-  A C_ ( A vH B )
4 1 2 chjcli
 |-  ( A vH B ) e. CH
5 1 4 pjoml2i
 |-  ( A C_ ( A vH B ) -> ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B ) )
6 3 5 ax-mp
 |-  ( A vH ( ( _|_ ` A ) i^i ( A vH B ) ) ) = ( A vH B )