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 ) )