Metamath Proof Explorer

Theorem pjoml4i

Description: Variation of orthomodular law. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 
|- A e. CH
pjoml2.2 
|- B e. CH
Assertion pjoml4i 
|- ( A vH ( B 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 inss1 
 |-  ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ B
4 1 choccli 
 |-  ( _|_ ` A ) e. CH
5 2 choccli 
 |-  ( _|_ ` B ) e. CH
6 4 5 chjcli 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) e. CH
7 2 6 chincli 
 |-  ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) e. CH
8 7 2 1 chlej2i 
 |-  ( ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ B -> ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) C_ ( A vH B ) )
9 3 8 ax-mp 
 |-  ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) C_ ( A vH B )
10 1 7 chub1i 
 |-  A C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) )
11 1 2 chdmm1i 
 |-  ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) )
12 11 ineq1i 
 |-  ( ( _|_ ` ( A i^i B ) ) i^i B ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i B )
13 incom 
 |-  ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i B ) = ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
14 12 13 eqtri 
 |-  ( ( _|_ ` ( A i^i B ) ) i^i B ) = ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) )
15 14 oveq2i 
 |-  ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = ( ( A i^i B ) vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) )
16 inss2 
 |-  ( A i^i B ) C_ B
17 1 2 chincli 
 |-  ( A i^i B ) e. CH
18 17 2 pjoml2i 
 |-  ( ( A i^i B ) C_ B -> ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = B )
19 16 18 ax-mp 
 |-  ( ( A i^i B ) vH ( ( _|_ ` ( A i^i B ) ) i^i B ) ) = B
20 15 19 eqtr3i 
 |-  ( ( A i^i B ) vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) = B
21 inss1 
 |-  ( A i^i B ) C_ A
22 17 1 7 chlej1i 
 |-  ( ( A i^i B ) C_ A -> ( ( A i^i B ) vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) )
23 21 22 ax-mp 
 |-  ( ( A i^i B ) vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) )
24 20 23 eqsstrri 
 |-  B C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) )
25 1 7 chjcli 
 |-  ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) e. CH
26 1 2 25 chlubii 
 |-  ( ( A C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) /\ B C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) ) -> ( A vH B ) C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) )
27 10 24 26 mp2an 
 |-  ( A vH B ) C_ ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) )
28 9 27 eqssi 
 |-  ( A vH ( B i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) ) = ( A vH B )