Metamath Proof Explorer

Theorem fh3i

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 fh3i ⊢ A ∨ ℋ B ∩ C = A ∨ ℋ B ∩ A ∨ ℋ 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 fh1i ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A ∩ ⊥ ⁡ C
14 2 3 chdmm1i ⊢ ⊥ ⁡ B ∩ C = ⊥ ⁡ B ∨ ℋ ⊥ ⁡ C
15 14 ineq2i ⊢ ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ C
16 1 2 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ B = ⊥ ⁡ A ∩ ⊥ ⁡ B
17 1 3 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ C = ⊥ ⁡ A ∩ ⊥ ⁡ C
18 16 17 oveq12i ⊢ ⊥ ⁡ A ∨ ℋ B ∨ ℋ ⊥ ⁡ A ∨ ℋ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∨ ℋ ⊥ ⁡ A ∩ ⊥ ⁡ C
19 13 15 18 3eqtr4ri ⊢ ⊥ ⁡ A ∨ ℋ B ∨ ℋ ⊥ ⁡ A ∨ ℋ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ C
20 1 2 chjcli ⊢ A ∨ ℋ B ∈ C ℋ
21 1 3 chjcli ⊢ A ∨ ℋ C ∈ C ℋ
22 20 21 chdmm1i ⊢ ⊥ ⁡ A ∨ ℋ B ∩ A ∨ ℋ C = ⊥ ⁡ A ∨ ℋ B ∨ ℋ ⊥ ⁡ A ∨ ℋ C
23 2 3 chincli ⊢ B ∩ C ∈ C ℋ
24 1 23 chdmj1i ⊢ ⊥ ⁡ A ∨ ℋ B ∩ C = ⊥ ⁡ A ∩ ⊥ ⁡ B ∩ C
25 19 22 24 3eqtr4i ⊢ ⊥ ⁡ A ∨ ℋ B ∩ A ∨ ℋ C = ⊥ ⁡ A ∨ ℋ B ∩ C
26 1 23 chjcli ⊢ A ∨ ℋ B ∩ C ∈ C ℋ
27 20 21 chincli ⊢ A ∨ ℋ B ∩ A ∨ ℋ C ∈ C ℋ
28 26 27 chcon3i ⊢ A ∨ ℋ B ∩ C = A ∨ ℋ B ∩ A ∨ ℋ C ↔ ⊥ ⁡ A ∨ ℋ B ∩ A ∨ ℋ C = ⊥ ⁡ A ∨ ℋ B ∩ C
29 25 28 mpbir ⊢ A ∨ ℋ B ∩ C = A ∨ ℋ B ∩ A ∨ ℋ C