Metamath Proof Explorer

Theorem osumcori

Description: Corollary of osumi . (Contributed by NM, 5-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses osum.1 
|- A e. CH
osum.2 
|- B e. CH
Assertion osumcori 
|- ( ( A i^i B ) +H ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) )

Proof

Step Hyp Ref Expression
1 osum.1 
 |-  A e. CH
2 osum.2 
 |-  B e. CH
3 inss2 
 |-  ( A i^i B ) C_ B
4 1 choccli 
 |-  ( _|_ ` A ) e. CH
5 2 4 chub2i 
 |-  B C_ ( ( _|_ ` A ) vH B )
6 3 5 sstri 
 |-  ( A i^i B ) C_ ( ( _|_ ` A ) vH B )
7 1 2 chdmm3i 
 |-  ( _|_ ` ( A i^i ( _|_ ` B ) ) ) = ( ( _|_ ` A ) vH B )
8 6 7 sseqtrri 
 |-  ( A i^i B ) C_ ( _|_ ` ( A i^i ( _|_ ` B ) ) )
9 1 2 chincli 
 |-  ( A i^i B ) e. CH
10 2 choccli 
 |-  ( _|_ ` B ) e. CH
11 1 10 chincli 
 |-  ( A i^i ( _|_ ` B ) ) e. CH
12 9 11 osumi 
 |-  ( ( A i^i B ) C_ ( _|_ ` ( A i^i ( _|_ ` B ) ) ) -> ( ( A i^i B ) +H ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) ) )
13 8 12 ax-mp 
 |-  ( ( A i^i B ) +H ( A i^i ( _|_ ` B ) ) ) = ( ( A i^i B ) vH ( A i^i ( _|_ ` B ) ) )