Metamath Proof Explorer


Theorem fh2i

Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Second 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 e. CH
fh1.2
|- B e. CH
fh1.3
|- C e. CH
fh1.4
|- A C_H B
fh1.5
|- A C_H C
Assertion fh2i
|- ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) )

Proof

Step Hyp Ref Expression
1 fh1.1
 |-  A e. CH
2 fh1.2
 |-  B e. CH
3 fh1.3
 |-  C e. CH
4 fh1.4
 |-  A C_H B
5 fh1.5
 |-  A C_H C
6 2 1 3 3pm3.2i
 |-  ( B e. CH /\ A e. CH /\ C e. CH )
7 4 5 pm3.2i
 |-  ( A C_H B /\ A C_H C )
8 fh2
 |-  ( ( ( B e. CH /\ A e. CH /\ C e. CH ) /\ ( A C_H B /\ A C_H C ) ) -> ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) ) )
9 6 7 8 mp2an
 |-  ( B i^i ( A vH C ) ) = ( ( B i^i A ) vH ( B i^i C ) )