This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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