Theorem cvexchi

Description: The Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of Kalmbach p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chpssat.1	|- A e. CH
	chpssat.2	|- B e. CH
Assertion	cvexchi	|- ( ( A i^i B ) A

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	|- A e. CH
2		chpssat.2	|- B e. CH
3	1 2	cvexchlem	|- ( ( A i^i B ) A
4	2	choccli	|- ( _|_ ` B ) e. CH
5	1	choccli	|- ( _|_ ` A ) e. CH
6	4 5	cvexchlem	|- ( ( ( _|_ ` B ) i^i ( _|_ ` A ) ) ( _|_ ` B )
7	1 2	chdmj1i	|- ( _|_ ` ( A vH B ) ) = ( ( _|_ ` A ) i^i ( _|_ ` B ) )
8		incom	|- ( ( _|_ ` A ) i^i ( _|_ ` B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
9	7 8	eqtri	|- ( _|_ ` ( A vH B ) ) = ( ( _|_ ` B ) i^i ( _|_ ` A ) )
10	9	breq1i	|- ( ( _|_ ` ( A vH B ) ) ( ( _|_ ` B ) i^i ( _|_ ` A ) )
11	1 2	chdmm1i	|- ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` A ) vH ( _|_ ` B ) )
12	5 4	chjcomi	|- ( ( _|_ ` A ) vH ( _|_ ` B ) ) = ( ( _|_ ` B ) vH ( _|_ ` A ) )
13	11 12	eqtri	|- ( _|_ ` ( A i^i B ) ) = ( ( _|_ ` B ) vH ( _|_ ` A ) )
14	13	breq2i	|- ( ( _|_ ` B ) ( _|_ ` B )
15	6 10 14	3imtr4i	|- ( ( _|_ ` ( A vH B ) ) ( _|_ ` B )
16	1 2	chjcli	|- ( A vH B ) e. CH
17		cvcon3	|- ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( A ( _|_ ` ( A vH B ) )
18	1 16 17	mp2an	|- ( A ( _|_ ` ( A vH B ) )
19	1 2	chincli	|- ( A i^i B ) e. CH
20		cvcon3	|- ( ( ( A i^i B ) e. CH /\ B e. CH ) -> ( ( A i^i B ) ( _|_ ` B )
21	19 2 20	mp2an	|- ( ( A i^i B ) ( _|_ ` B )
22	15 18 21	3imtr4i	|- ( A ( A i^i B )
23	3 22	impbii	|- ( ( A i^i B ) A