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