This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjoml3i

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 pjoml2.1 
 |-  A e. CH
2 pjoml2.2 
 |-  B e. CH
3 1 choccli 
 |-  ( _|_ ` A ) e. CH
4 2 choccli 
 |-  ( _|_ ` B ) e. CH
5 3 4 pjoml2i 
 |-  ( ( _|_ ` A ) C_ ( _|_ ` B ) -> ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` B ) )
6 2 1 chsscon3i 
 |-  ( B C_ A <-> ( _|_ ` A ) C_ ( _|_ ` B ) )
7 eqcom 
 |-  ( ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) = B <-> B = ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) )
8 3 choccli 
 |-  ( _|_ ` ( _|_ ` A ) ) e. CH
9 8 4 chincli 
 |-  ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) e. CH
10 1 9 chdmj2i 
 |-  ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) = ( A i^i ( _|_ ` ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) )
11 3 2 chdmm4i 
 |-  ( _|_ ` ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B )
12 11 ineq2i 
 |-  ( A i^i ( _|_ ` ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) )
13 10 12 eqtri 
 |-  ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) = ( A i^i ( ( _|_ ` A ) vH B ) )
14 13 eqeq1i 
 |-  ( ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) = B <-> ( A i^i ( ( _|_ ` A ) vH B ) ) = B )
15 3 9 chjcli 
 |-  ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) e. CH
16 2 15 chcon2i 
 |-  ( B = ( _|_ ` ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) ) <-> ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` B ) )
17 7 14 16 3bitr3i 
 |-  ( ( A i^i ( ( _|_ ` A ) vH B ) ) = B <-> ( ( _|_ ` A ) vH ( ( _|_ ` ( _|_ ` A ) ) i^i ( _|_ ` B ) ) ) = ( _|_ ` B ) )
18 5 6 17 3imtr4i 
 |-  ( B C_ A -> ( A i^i ( ( _|_ ` A ) vH B ) ) = B )