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 ⊢ 𝐴 ∈ Cℋ
osum.2 ⊢ 𝐵 ∈ Cℋ
Assertion osumcor2i ( 𝐴 𝐶ℋ 𝐵 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 osum.1 ⊢ 𝐴 ∈ Cℋ
2 osum.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 cmcm2i ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) )
4 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
5 1 4 cmbr4i ⊢ ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ 𝐵 ) )
6 3 5 bitri ⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ 𝐵 ) )
7 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
8 7 4 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
9 1 8 chincli ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
10 9 2 osumi ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) )
11 7 4 chjcomi ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) = ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) )
12 11 ineq2i ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) )
13 12 oveq1i ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) = ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∨ℋ 𝐵 )
14 4 7 chjcli ⊢ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ
15 1 14 chincli ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∈ Cℋ
16 15 2 chjcomi ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) )
17 13 16 eqtri ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) = ( 𝐵 ∨ℋ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) )
18 2 1 pjoml4i ⊢ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ) = ( 𝐵 ∨ℋ 𝐴 )
19 2 1 chjcomi ⊢ ( 𝐵 ∨ℋ 𝐴 ) = ( 𝐴 ∨ℋ 𝐵 )
20 18 19 eqtri ⊢ ( 𝐵 ∨ℋ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐵 ) ∨ℋ ( ⊥ ‘ 𝐴 ) ) ) ) = ( 𝐴 ∨ℋ 𝐵 )
21 17 20 eqtri ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 )
22 21 eqeq2i ⊢ ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) ↔ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )
23 inss1 ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐴
24 9 chshii ⊢ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∈ Sℋ
25 1 chshii ⊢ 𝐴 ∈ Sℋ
26 2 chshii ⊢ 𝐵 ∈ Sℋ
27 24 25 26 shlessi ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐴 → ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
28 23 27 ax-mp ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 )
29 sseq1 ⊢ ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
30 28 29 mpbii ⊢ ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
31 22 30 sylbi ⊢ ( ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) +ℋ 𝐵 ) = ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ 𝐵 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
32 10 31 syl ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ ( ⊥ ‘ 𝐵 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
33 6 32 sylbi ⊢ ( 𝐴 𝐶ℋ 𝐵 → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) )
34 1 2 chsleji ⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
35 33 34 jctil ⊢ ( 𝐴 𝐶ℋ 𝐵 → ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
36 eqss ⊢ ( ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) ↔ ( ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) )
37 35 36 sylibr ⊢ ( 𝐴 𝐶ℋ 𝐵 → ( 𝐴 +ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐵 ) )