Theorem cvexch

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, 21-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	cvexch	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B$$
2	1	breq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\right)$$
3		id	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)$$
4		oveq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A{\vee }_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B$$
5	3 4	breq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\right)$$
6	2 5	bibi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\right)\right)$$
7		ineq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
8		id	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
9	7 8	breq12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
10		oveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
11	10	breq2d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
12	9 11	bibi12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)\right)$$
13		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15	13 14	cvexchi	$$⊢\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right){⋖}_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){⋖}_{\mathscr{H}}\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
16	6 12 15	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(A\cap B\right){⋖}_{\mathscr{H}}B\leftrightarrow A{⋖}_{\mathscr{H}}\left(A{\vee }_{\mathscr{H}}B\right)\right)$$