# Metamath Proof Explorer

## Theorem fh1i

Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of Kalmbach p. 25. (Contributed by NM, 7-Aug-2004) (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 fh1i ${⊢}{A}\cap \left({B}{\vee }_{ℋ}{C}\right)=\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {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 2 3 3pm3.2i ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)$
7 4 5 pm3.2i ${⊢}\left({A}{𝐶}_{ℋ}{B}\wedge {A}{𝐶}_{ℋ}{C}\right)$
8 fh1 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝐶}_{ℋ}{B}\wedge {A}{𝐶}_{ℋ}{C}\right)\right)\to {A}\cap \left({B}{\vee }_{ℋ}{C}\right)=\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {C}\right)$
9 6 7 8 mp2an ${⊢}{A}\cap \left({B}{\vee }_{ℋ}{C}\right)=\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {C}\right)$