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

Metamath Proof Explorer

Theorem osumcori

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

Ref Expression
Hypotheses osum.1 ⊢ 𝐴 ∈ Cℋ
osum.2 ⊢ 𝐵 ∈ Cℋ
Assertion osumcori ( ( 𝐴 ∩ 𝐵 ) +ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 osum.1 ⊢ 𝐴 ∈ Cℋ
2 osum.2 ⊢ 𝐵 ∈ Cℋ
3 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
4 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5 2 4 chub2i ⊢ 𝐵 ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
6 3 5 sstri ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
7 1 2 chdmm3i ⊢ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
8 6 7 sseqtrri ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )
9 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
10 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
11 1 10 chincli ⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
12 9 11 osumi ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ ( ⊥ ‘ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) → ( ( 𝐴 ∩ 𝐵 ) +ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) )
13 8 12 ax-mp ⊢ ( ( 𝐴 ∩ 𝐵 ) +ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )