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

Metamath Proof Explorer

Theorem lejdii

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

Proof

Step Hyp Ref Expression
1 ledi.1 ⊢ 𝐴 ∈ Cℋ
2 ledi.2 ⊢ 𝐵 ∈ Cℋ
3 ledi.3 ⊢ 𝐶 ∈ Cℋ
4 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
5 1 3 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 )
6 4 5 ssini ⊢ 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) )
7 inss1 ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵
8 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
9 7 8 sstri ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 )
10 inss2 ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶
11 3 1 chub2i ⊢ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 )
12 10 11 sstri ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐶 )
13 9 12 ssini ⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) )
14 2 3 chincli ⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ
15 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
16 1 3 chjcli ⊢ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ
17 15 16 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∈ Cℋ
18 1 14 17 chlubi ⊢ ( ( 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∧ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ) ↔ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) )
19 18 bicomi ⊢ ( ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ↔ ( 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∧ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ) )
20 6 13 19 mpbir2an ⊢ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) )