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

Metamath Proof Explorer

Theorem fh2i

Proof