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}}_{\mathscr{H}}$$
	fh1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	fh1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	fh1.4	$$⊢A{𝐶}_{\mathscr{H}}B$$
	fh1.5	$$⊢A{𝐶}_{\mathscr{H}}C$$
Assertion	fh1i	$$⊢A\cap \left(B{\vee }_{\mathscr{H}}C\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$

Proof

Step	Hyp	Ref	Expression
1		fh1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		fh1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		fh1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		fh1.4	$$⊢A{𝐶}_{\mathscr{H}}B$$
5		fh1.5	$$⊢A{𝐶}_{\mathscr{H}}C$$
6	1 2 3	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)$$
7	4 5	pm3.2i	$$⊢\left(A{𝐶}_{\mathscr{H}}B\wedge A{𝐶}_{\mathscr{H}}C\right)$$
8		fh1	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝐶}_{\mathscr{H}}B\wedge A{𝐶}_{\mathscr{H}}C\right)\right)\to A\cap \left(B{\vee }_{\mathscr{H}}C\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$
9	6 7 8	mp2an	$$⊢A\cap \left(B{\vee }_{\mathscr{H}}C\right)=\left(A\cap B\right){\vee }_{\mathscr{H}}\left(A\cap C\right)$$