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 𝐴C
pjoml2.2 𝐵C
Assertion pjoml5i ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 𝐴C
2 pjoml2.2 𝐵C
3 1 2 chub1i 𝐴 ⊆ ( 𝐴 𝐵 )
4 1 2 chjcli ( 𝐴 𝐵 ) ∈ C
5 1 4 pjoml2i ( 𝐴 ⊆ ( 𝐴 𝐵 ) → ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 𝐵 ) )
6 3 5 ax-mp ( 𝐴 ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 𝐵 ) ) ) = ( 𝐴 𝐵 )