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

Metamath Proof Explorer

Theorem chjassi

Description: Associative law for Hilbert lattice join. From definition of lattice in Kalmbach p. 14. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 
|- A e. CH
chjcl.2 
|- B e. CH
chjass.3 
|- C e. CH
Assertion chjassi 
|- ( ( A vH B ) vH C ) = ( A vH ( B vH C ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 chjcl.2 
 |-  B e. CH
3 chjass.3 
 |-  C e. CH
4 inass 
 |-  ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) i^i ( _|_ ` C ) ) = ( ( _|_ ` A ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) )
5 1 2 chdmj1i 
 |-  ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
6 5 ineq1i 
 |-  ( ( _|_ ` ( A vH B ) ) i^i ( _|_ ` C ) ) = ( ( ( _|_ ` A ) i^i ( _|_ ` B ) ) i^i ( _|_ ` C ) )
7 2 3 chdmj1i 
 |-  ( _|_ ` ( B vH C ) ) = ( ( _|_ ` B ) i^i ( _|_ ` C ) )
8 7 ineq2i 
 |-  ( ( _|_ ` A ) i^i ( _|_ ` ( B vH C ) ) ) = ( ( _|_ ` A ) i^i ( ( _|_ ` B ) i^i ( _|_ ` C ) ) )
9 4 6 8 3eqtr4i 
 |-  ( ( _|_ ` ( A vH B ) ) i^i ( _|_ ` C ) ) = ( ( _|_ ` A ) i^i ( _|_ ` ( B vH C ) ) )
10 9 fveq2i 
 |-  ( _|_ ` ( ( _|_ ` ( A vH B ) ) i^i ( _|_ ` C ) ) ) = ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` ( B vH C ) ) ) )
11 1 2 chjcli 
 |-  ( A vH B ) e. CH
12 11 3 chdmm4i 
 |-  ( _|_ ` ( ( _|_ ` ( A vH B ) ) i^i ( _|_ ` C ) ) ) = ( ( A vH B ) vH C )
13 2 3 chjcli 
 |-  ( B vH C ) e. CH
14 1 13 chdmm4i 
 |-  ( _|_ ` ( ( _|_ ` A ) i^i ( _|_ ` ( B vH C ) ) ) ) = ( A vH ( B vH C ) )
15 10 12 14 3eqtr3i 
 |-  ( ( A vH B ) vH C ) = ( A vH ( B vH C ) )