Theorem omlsi

Description: Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of Kalmbach p. 22. (Contributed by NM, 14-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	omls.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	omls.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
Assertion	omlsi	$$⊢\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right)\to A=B$$

Proof

Step	Hyp	Ref	Expression
1		omls.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		omls.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		eqeq1	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(A=B\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)=B\right)$$
4		eqeq2	$$⊢B=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)=B\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\right)$$
5		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
6	1 5	ifcli	$$⊢if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
7		h0elsh	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}$$
8	2 7	ifcli	$$⊢if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\in {\mathbf{S}}_{\mathscr{H}}$$
9		sseq1	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(A\subseteq B\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq B\right)$$
10		fveq2	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \perp \left(A\right)=\perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
11	10	ineq2d	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to B\cap \perp \left(A\right)=B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
12	11	eqeq1d	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(B\cap \perp \left(A\right)=0_{\mathscr{H}}\leftrightarrow B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
13	9 12	anbi12d	$$⊢A=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right)\leftrightarrow \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq B\wedge B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\right)$$
14		sseq2	$$⊢B=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq B\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\right)$$
15		ineq1	$$⊢B=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
16	15	eqeq1d	$$⊢B=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
17	14 16	anbi12d	$$⊢B=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(\left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq B\wedge B\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\leftrightarrow \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\wedge if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\right)$$
18		sseq1	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq 0_{\mathscr{H}}\right)$$
19		fveq2	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \perp \left(0_{\mathscr{H}}\right)=\perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
20	19	ineq2d	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to 0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
21	20	eqeq1d	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}\leftrightarrow 0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
22	18 21	anbi12d	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\to \left(\left(0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}\right)\leftrightarrow \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\right)$$
23		sseq2	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq 0_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\right)$$
24		ineq1	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to 0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)$$
25	24	eqeq1d	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\leftrightarrow if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
26	23 25	anbi12d	$$⊢0_{\mathscr{H}}=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\to \left(\left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\leftrightarrow \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\wedge if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)\right)$$
27		ssid	$$⊢0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}$$
28		ocin	$$⊢0_{\mathscr{H}}\in {\mathbf{S}}_{\mathscr{H}}\to 0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
29	7 28	ax-mp	$$⊢0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}$$
30	27 29	pm3.2i	$$⊢\left(0_{\mathscr{H}}\subseteq 0_{\mathscr{H}}\wedge 0_{\mathscr{H}}\cap \perp \left(0_{\mathscr{H}}\right)=0_{\mathscr{H}}\right)$$
31	13 17 22 26 30	elimhyp2v	$$⊢\left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\wedge if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}\right)$$
32	31	simpli	$$⊢if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\subseteq if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)$$
33	31	simpri	$$⊢if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)\cap \perp \left(if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)\right)=0_{\mathscr{H}}$$
34	6 8 32 33	omlsii	$$⊢if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),A,0_{\mathscr{H}}\right)=if\left(\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right),B,0_{\mathscr{H}}\right)$$
35	3 4 34	dedth2v	$$⊢\left(A\subseteq B\wedge B\cap \perp \left(A\right)=0_{\mathscr{H}}\right)\to A=B$$