This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝐵 ∩ ( 𝐴 ∨ℋ 𝐶 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) )