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 𝐴C
fh1.2 𝐵C
fh1.3 𝐶C
fh1.4 𝐴 𝐶 𝐵
fh1.5 𝐴 𝐶 𝐶
Assertion fh2i ( 𝐵 ∩ ( 𝐴 𝐶 ) ) = ( ( 𝐵𝐴 ) ∨ ( 𝐵𝐶 ) )

Proof

Step Hyp Ref Expression
1 fh1.1 𝐴C
2 fh1.2 𝐵C
3 fh1.3 𝐶C
4 fh1.4 𝐴 𝐶 𝐵
5 fh1.5 𝐴 𝐶 𝐶
6 2 1 3 3pm3.2i ( 𝐵C𝐴C𝐶C )
7 4 5 pm3.2i ( 𝐴 𝐶 𝐵𝐴 𝐶 𝐶 )
8 fh2 ( ( ( 𝐵C𝐴C𝐶C ) ∧ ( 𝐴 𝐶 𝐵𝐴 𝐶 𝐶 ) ) → ( 𝐵 ∩ ( 𝐴 𝐶 ) ) = ( ( 𝐵𝐴 ) ∨ ( 𝐵𝐶 ) ) )
9 6 7 8 mp2an ( 𝐵 ∩ ( 𝐴 𝐶 ) ) = ( ( 𝐵𝐴 ) ∨ ( 𝐵𝐶 ) )