Metamath Proof Explorer

Theorem fh4i

Description: Variation of the Foulis-Holland Theorem. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

Ref Expression
Hypotheses fh1.1 ⊢ A ∈ C ℋ
fh1.2 ⊢ B ∈ C ℋ
fh1.3 ⊢ C ∈ C ℋ
fh1.4 ⊢ A 𝐶 ℋ B
fh1.5 ⊢ A 𝐶 ℋ C
Assertion fh4i ⊢ B ∨ ℋ A ∩ C = B ∨ ℋ A ∩ B ∨ ℋ C

Proof

Step Hyp Ref Expression
1 fh1.1 ⊢ A ∈ C ℋ
2 fh1.2 ⊢ B ∈ C ℋ
3 fh1.3 ⊢ C ∈ C ℋ
4 fh1.4 ⊢ A 𝐶 ℋ B
5 fh1.5 ⊢ A 𝐶 ℋ C
6 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
7 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
8 3 choccli ⊢ ⊥ ⁡ C ∈ C ℋ
9 1 2 4 cmcm3ii ⊢ ⊥ ⁡ A 𝐶 ℋ B
10 6 2 9 cmcm2ii ⊢ ⊥ ⁡ A 𝐶 ℋ ⊥ ⁡ B
11 1 3 5 cmcm3ii ⊢ ⊥ ⁡ A 𝐶 ℋ C
12 6 3 11 cmcm2ii ⊢ ⊥ ⁡ A 𝐶 ℋ ⊥ ⁡ C
13 6 7 8 10 12 fh2i ⊢ ⊥ ⁡ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ C = ⊥ ⁡ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∩ ⊥ ⁡ C
14 1 3 chdmm1i ⊢ ⊥ ⁡ A ∩ C = ⊥ ⁡ A ∨ ℋ ⊥ ⁡ C
15 14 ineq2i ⊢ ⊥ ⁡ B ∩ ⊥ ⁡ A ∩ C = ⊥ ⁡ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ C
16 2 1 chdmj1i ⊢ ⊥ ⁡ B ∨ ℋ A = ⊥ ⁡ B ∩ ⊥ ⁡ A
17 2 3 chdmj1i ⊢ ⊥ ⁡ B ∨ ℋ C = ⊥ ⁡ B ∩ ⊥ ⁡ C
18 16 17 oveq12i ⊢ ⊥ ⁡ B ∨ ℋ A ∨ ℋ ⊥ ⁡ B ∨ ℋ C = ⊥ ⁡ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∩ ⊥ ⁡ C
19 13 15 18 3eqtr4ri ⊢ ⊥ ⁡ B ∨ ℋ A ∨ ℋ ⊥ ⁡ B ∨ ℋ C = ⊥ ⁡ B ∩ ⊥ ⁡ A ∩ C
20 2 1 chjcli ⊢ B ∨ ℋ A ∈ C ℋ
21 2 3 chjcli ⊢ B ∨ ℋ C ∈ C ℋ
22 20 21 chdmm1i ⊢ ⊥ ⁡ B ∨ ℋ A ∩ B ∨ ℋ C = ⊥ ⁡ B ∨ ℋ A ∨ ℋ ⊥ ⁡ B ∨ ℋ C
23 1 3 chincli ⊢ A ∩ C ∈ C ℋ
24 2 23 chdmj1i ⊢ ⊥ ⁡ B ∨ ℋ A ∩ C = ⊥ ⁡ B ∩ ⊥ ⁡ A ∩ C
25 19 22 24 3eqtr4i ⊢ ⊥ ⁡ B ∨ ℋ A ∩ B ∨ ℋ C = ⊥ ⁡ B ∨ ℋ A ∩ C
26 2 23 chjcli ⊢ B ∨ ℋ A ∩ C ∈ C ℋ
27 20 21 chincli ⊢ B ∨ ℋ A ∩ B ∨ ℋ C ∈ C ℋ
28 26 27 chcon3i ⊢ B ∨ ℋ A ∩ C = B ∨ ℋ A ∩ B ∨ ℋ C ↔ ⊥ ⁡ B ∨ ℋ A ∩ B ∨ ℋ C = ⊥ ⁡ B ∨ ℋ A ∩ C
29 25 28 mpbir ⊢ B ∨ ℋ A ∩ C = B ∨ ℋ A ∩ B ∨ ℋ C