Theorem ledii

Description: An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ledi.1	⊢ 𝐴 ∈ Cℋ
2		ledi.2	⊢ 𝐵 ∈ Cℋ
3		ledi.3	⊢ 𝐶 ∈ Cℋ
4		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
5		inss1	⊢ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴
6	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
7	1 3	chincli	⊢ ( 𝐴 ∩ 𝐶 ) ∈ Cℋ
8	6 7 1	chlubii	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ∧ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ 𝐴 )
9	4 5 8	mp2an	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ 𝐴
10		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
11		inss2	⊢ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐶
12	6 2 7 3	chlej12i	⊢ ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐴 ∩ 𝐶 ) ⊆ 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐵 ∨ℋ 𝐶 ) )
13	10 11 12	mp2an	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐵 ∨ℋ 𝐶 )
14	9 13	ssini	⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 ∨ℋ 𝐶 ) )