Metamath Proof Explorer

Theorem osumcor2i

Description: Corollary of osumi , showing it holds under the weaker hypothesis that A and B commute. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses osum.1 
|- A e. CH
osum.2 
|- B e. CH
Assertion osumcor2i 
|- ( A C_H B -> ( A +H B ) = ( A vH B ) )

Proof

Step Hyp Ref Expression
1 osum.1 
 |-  A e. CH
2 osum.2 
 |-  B e. CH
3 1 2 cmcm2i 
 |-  ( A C_H B <-> A C_H ( _|_ ` B ) )
4 2 choccli 
 |-  ( _|_ ` B ) e. CH
5 1 4 cmbr4i 
 |-  ( A C_H ( _|_ ` B ) <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ ( _|_ ` B ) )
6 3 5 bitri 
 |-  ( A C_H B <-> ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ ( _|_ ` B ) )
7 1 choccli 
 |-  ( _|_ ` A ) e. CH
8 7 4 chjcli 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) e. CH
9 1 8 chincli 
 |-  ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) e. CH
10 9 2 osumi 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ ( _|_ ` B ) -> ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) )
11 7 4 chjcomi 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) = ( ( _|_ ` B ) vH ( _|_ ` A ) )
12 11 ineq2i 
 |-  ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) )
13 12 oveq1i 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) = ( ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) vH B )
14 4 7 chjcli 
 |-  ( ( _|_ ` B ) vH ( _|_ ` A ) ) e. CH
15 1 14 chincli 
 |-  ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) e. CH
16 15 2 chjcomi 
 |-  ( ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) vH B ) = ( B vH ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) )
17 13 16 eqtri 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) = ( B vH ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) )
18 2 1 pjoml4i 
 |-  ( B vH ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) ) = ( B vH A )
19 2 1 chjcomi 
 |-  ( B vH A ) = ( A vH B )
20 18 19 eqtri 
 |-  ( B vH ( A i^i ( ( _|_ ` B ) vH ( _|_ ` A ) ) ) ) = ( A vH B )
21 17 20 eqtri 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) = ( A vH B )
22 21 eqeq2i 
 |-  ( ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) <-> ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( A vH B ) )
23 inss1 
 |-  ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ A
24 9 chshii 
 |-  ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) e. SH
25 1 chshii 
 |-  A e. SH
26 2 chshii 
 |-  B e. SH
27 24 25 26 shlessi 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ A -> ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) C_ ( A +H B ) )
28 23 27 ax-mp 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) C_ ( A +H B )
29 sseq1 
 |-  ( ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( A vH B ) -> ( ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) C_ ( A +H B ) <-> ( A vH B ) C_ ( A +H B ) ) )
30 28 29 mpbii 
 |-  ( ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( A vH B ) -> ( A vH B ) C_ ( A +H B ) )
31 22 30 sylbi 
 |-  ( ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) +H B ) = ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH B ) -> ( A vH B ) C_ ( A +H B ) )
32 10 31 syl 
 |-  ( ( A i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) C_ ( _|_ ` B ) -> ( A vH B ) C_ ( A +H B ) )
33 6 32 sylbi 
 |-  ( A C_H B -> ( A vH B ) C_ ( A +H B ) )
34 1 2 chsleji 
 |-  ( A +H B ) C_ ( A vH B )
35 33 34 jctil 
 |-  ( A C_H B -> ( ( A +H B ) C_ ( A vH B ) /\ ( A vH B ) C_ ( A +H B ) ) )
36 eqss 
 |-  ( ( A +H B ) = ( A vH B ) <-> ( ( A +H B ) C_ ( A vH B ) /\ ( A vH B ) C_ ( A +H B ) ) )
37 35 36 sylibr 
 |-  ( A C_H B -> ( A +H B ) = ( A vH B ) )