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 
|- A e. CH
ledi.2 
|- B e. CH
ledi.3 
|- C e. CH
Assertion lejdii 
|- ( A vH ( B i^i C ) ) C_ ( ( A vH B ) i^i ( A vH C ) )

Proof

Step Hyp Ref Expression
1 ledi.1 
 |-  A e. CH
2 ledi.2 
 |-  B e. CH
3 ledi.3 
 |-  C e. CH
4 1 2 chub1i 
 |-  A C_ ( A vH B )
5 1 3 chub1i 
 |-  A C_ ( A vH C )
6 4 5 ssini 
 |-  A C_ ( ( A vH B ) i^i ( A vH C ) )
7 inss1 
 |-  ( B i^i C ) C_ B
8 2 1 chub2i 
 |-  B C_ ( A vH B )
9 7 8 sstri 
 |-  ( B i^i C ) C_ ( A vH B )
10 inss2 
 |-  ( B i^i C ) C_ C
11 3 1 chub2i 
 |-  C C_ ( A vH C )
12 10 11 sstri 
 |-  ( B i^i C ) C_ ( A vH C )
13 9 12 ssini 
 |-  ( B i^i C ) C_ ( ( A vH B ) i^i ( A vH C ) )
14 2 3 chincli 
 |-  ( B i^i C ) e. CH
15 1 2 chjcli 
 |-  ( A vH B ) e. CH
16 1 3 chjcli 
 |-  ( A vH C ) e. CH
17 15 16 chincli 
 |-  ( ( A vH B ) i^i ( A vH C ) ) e. CH
18 1 14 17 chlubi 
 |-  ( ( A C_ ( ( A vH B ) i^i ( A vH C ) ) /\ ( B i^i C ) C_ ( ( A vH B ) i^i ( A vH C ) ) ) <-> ( A vH ( B i^i C ) ) C_ ( ( A vH B ) i^i ( A vH C ) ) )
19 18 bicomi 
 |-  ( ( A vH ( B i^i C ) ) C_ ( ( A vH B ) i^i ( A vH C ) ) <-> ( A C_ ( ( A vH B ) i^i ( A vH C ) ) /\ ( B i^i C ) C_ ( ( A vH B ) i^i ( A vH C ) ) ) )
20 6 13 19 mpbir2an 
 |-  ( A vH ( B i^i C ) ) C_ ( ( A vH B ) i^i ( A vH C ) )