Theorem lejdiri

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

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

Proof

Step	Hyp	Ref	Expression
1		ledi.1	⊢ 𝐴 ∈ Cℋ
2		ledi.2	⊢ 𝐵 ∈ Cℋ
3		ledi.3	⊢ 𝐶 ∈ Cℋ
4	3 1 2	lejdii	⊢ ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐶 ∨ℋ 𝐵 ) )
5	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
6	5 3	chjcomi	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ ( 𝐴 ∩ 𝐵 ) )
7	1 3	chjcomi	⊢ ( 𝐴 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐴 )
8	2 3	chjcomi	⊢ ( 𝐵 ∨ℋ 𝐶 ) = ( 𝐶 ∨ℋ 𝐵 )
9	7 8	ineq12i	⊢ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) ) = ( ( 𝐶 ∨ℋ 𝐴 ) ∩ ( 𝐶 ∨ℋ 𝐵 ) )
10	4 6 9	3sstr4i	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐶 ) ∩ ( 𝐵 ∨ℋ 𝐶 ) )