Theorem lediri

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ledi.1	⊢ 𝐴 ∈ Cℋ
	ledi.2	⊢ 𝐵 ∈ Cℋ
	ledi.3	⊢ 𝐶 ∈ Cℋ
Assertion	lediri	⊢ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		ledi.1	⊢ 𝐴 ∈ Cℋ
2		ledi.2	⊢ 𝐵 ∈ Cℋ
3		ledi.3	⊢ 𝐶 ∈ Cℋ
4	3 1 2	ledii	⊢ ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ⊆ ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
5		incom	⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐴 )
6		incom	⊢ ( 𝐵 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐵 )
7	5 6	oveq12i	⊢ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐶 ∩ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) )
8		incom	⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 ) = ( 𝐶 ∩ ( 𝐴 ∨ℋ 𝐵 ) )
9	4 7 8	3sstr4i	⊢ ( ( 𝐴 ∩ 𝐶 ) ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ 𝐶 )