# 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}\in {\mathbf{C}}_{ℋ}$
fh1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
fh1.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
fh1.4 ${⊢}{A}{𝐶}_{ℋ}{B}$
fh1.5 ${⊢}{A}{𝐶}_{ℋ}{C}$
Assertion fh3i ${⊢}{A}{\vee }_{ℋ}\left({B}\cap {C}\right)=\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)$

### Proof

Step Hyp Ref Expression
1 fh1.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 fh1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 fh1.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
4 fh1.4 ${⊢}{A}{𝐶}_{ℋ}{B}$
5 fh1.5 ${⊢}{A}{𝐶}_{ℋ}{C}$
6 1 choccli ${⊢}\perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
7 2 choccli ${⊢}\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
8 3 choccli ${⊢}\perp \left({C}\right)\in {\mathbf{C}}_{ℋ}$
9 1 2 4 cmcm3ii ${⊢}\perp \left({A}\right){𝐶}_{ℋ}{B}$
10 6 2 9 cmcm2ii ${⊢}\perp \left({A}\right){𝐶}_{ℋ}\perp \left({B}\right)$
11 1 3 5 cmcm3ii ${⊢}\perp \left({A}\right){𝐶}_{ℋ}{C}$
12 6 3 11 cmcm2ii ${⊢}\perp \left({A}\right){𝐶}_{ℋ}\perp \left({C}\right)$
13 6 7 8 10 12 fh1i ${⊢}\perp \left({A}\right)\cap \left(\perp \left({B}\right){\vee }_{ℋ}\perp \left({C}\right)\right)=\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({C}\right)\right)$
14 2 3 chdmm1i ${⊢}\perp \left({B}\cap {C}\right)=\perp \left({B}\right){\vee }_{ℋ}\perp \left({C}\right)$
15 14 ineq2i ${⊢}\perp \left({A}\right)\cap \perp \left({B}\cap {C}\right)=\perp \left({A}\right)\cap \left(\perp \left({B}\right){\vee }_{ℋ}\perp \left({C}\right)\right)$
16 1 2 chdmj1i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right)=\perp \left({A}\right)\cap \perp \left({B}\right)$
17 1 3 chdmj1i ${⊢}\perp \left({A}{\vee }_{ℋ}{C}\right)=\perp \left({A}\right)\cap \perp \left({C}\right)$
18 16 17 oveq12i ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{C}\right)=\left(\perp \left({A}\right)\cap \perp \left({B}\right)\right){\vee }_{ℋ}\left(\perp \left({A}\right)\cap \perp \left({C}\right)\right)$
19 13 15 18 3eqtr4ri ${⊢}\perp \left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{C}\right)=\perp \left({A}\right)\cap \perp \left({B}\cap {C}\right)$
20 1 2 chjcli ${⊢}{A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
21 1 3 chjcli ${⊢}{A}{\vee }_{ℋ}{C}\in {\mathbf{C}}_{ℋ}$
22 20 21 chdmm1i ${⊢}\perp \left(\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)\right)=\perp \left({A}{\vee }_{ℋ}{B}\right){\vee }_{ℋ}\perp \left({A}{\vee }_{ℋ}{C}\right)$
23 2 3 chincli ${⊢}{B}\cap {C}\in {\mathbf{C}}_{ℋ}$
24 1 23 chdmj1i ${⊢}\perp \left({A}{\vee }_{ℋ}\left({B}\cap {C}\right)\right)=\perp \left({A}\right)\cap \perp \left({B}\cap {C}\right)$
25 19 22 24 3eqtr4i ${⊢}\perp \left(\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)\right)=\perp \left({A}{\vee }_{ℋ}\left({B}\cap {C}\right)\right)$
26 1 23 chjcli ${⊢}{A}{\vee }_{ℋ}\left({B}\cap {C}\right)\in {\mathbf{C}}_{ℋ}$
27 20 21 chincli ${⊢}\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)\in {\mathbf{C}}_{ℋ}$
28 26 27 chcon3i ${⊢}{A}{\vee }_{ℋ}\left({B}\cap {C}\right)=\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)↔\perp \left(\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)\right)=\perp \left({A}{\vee }_{ℋ}\left({B}\cap {C}\right)\right)$
29 25 28 mpbir ${⊢}{A}{\vee }_{ℋ}\left({B}\cap {C}\right)=\left({A}{\vee }_{ℋ}{B}\right)\cap \left({A}{\vee }_{ℋ}{C}\right)$