Metamath Proof Explorer

Theorem chj4

Description: Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion chj4 
|- ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) ) )

Proof

Step Hyp Ref Expression
1 chj12 
 |-  ( ( B e. CH /\ C e. CH /\ D e. CH ) -> ( B vH ( C vH D ) ) = ( C vH ( B vH D ) ) )
2 1 3expb 
 |-  ( ( B e. CH /\ ( C e. CH /\ D e. CH ) ) -> ( B vH ( C vH D ) ) = ( C vH ( B vH D ) ) )
3 2 adantll 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( B vH ( C vH D ) ) = ( C vH ( B vH D ) ) )
4 3 oveq2d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( A vH ( B vH ( C vH D ) ) ) = ( A vH ( C vH ( B vH D ) ) ) )
5 chjcl 
 |-  ( ( C e. CH /\ D e. CH ) -> ( C vH D ) e. CH )
6 chjass 
 |-  ( ( A e. CH /\ B e. CH /\ ( C vH D ) e. CH ) -> ( ( A vH B ) vH ( C vH D ) ) = ( A vH ( B vH ( C vH D ) ) ) )
7 6 3expa 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C vH D ) e. CH ) -> ( ( A vH B ) vH ( C vH D ) ) = ( A vH ( B vH ( C vH D ) ) ) )
8 5 7 sylan2 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( A vH B ) vH ( C vH D ) ) = ( A vH ( B vH ( C vH D ) ) ) )
9 chjcl 
 |-  ( ( B e. CH /\ D e. CH ) -> ( B vH D ) e. CH )
10 chjass 
 |-  ( ( A e. CH /\ C e. CH /\ ( B vH D ) e. CH ) -> ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) ) )
11 10 3expa 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ ( B vH D ) e. CH ) -> ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) ) )
12 9 11 sylan2 
 |-  ( ( ( A e. CH /\ C e. CH ) /\ ( B e. CH /\ D e. CH ) ) -> ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) ) )
13 12 an4s 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( A vH C ) vH ( B vH D ) ) = ( A vH ( C vH ( B vH D ) ) ) )
14 4 8 13 3eqtr4d 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ ( C e. CH /\ D e. CH ) ) -> ( ( A vH B ) vH ( C vH D ) ) = ( ( A vH C ) vH ( B vH D ) ) )