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	⊢ ( ( 𝐴 ∩ 𝐵 ) +ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) )