Theorem omlsii

Description: Subspace inference form of orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999) (Revised by Mario Carneiro, 15-May-2014) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		omlsi.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		omlsi.2	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
3		omlsi.3	$$⊢A\subseteq B$$
4		omlsi.4	$$⊢B\cap \perp \left(A\right)=0_{\mathscr{H}}$$
5	2	sheli	$$⊢x\in B\to x\in \mathscr{H}$$
6	1 5	pjhthlem2	$$⊢x\in B\to \exists y\in A\exists z\in \perp \left(A\right)x=y{+}_{ℎ}z$$
7		eqeq1	$$⊢x=if\left(x\in B,x,0_{ℎ}\right)\to \left(x=y{+}_{ℎ}z\leftrightarrow if\left(x\in B,x,0_{ℎ}\right)=y{+}_{ℎ}z\right)$$
8		eleq1	$$⊢x=if\left(x\in B,x,0_{ℎ}\right)\to \left(x\in A\leftrightarrow if\left(x\in B,x,0_{ℎ}\right)\in A\right)$$
9	7 8	imbi12d	$$⊢x=if\left(x\in B,x,0_{ℎ}\right)\to \left(\left(x=y{+}_{ℎ}z\to x\in A\right)\leftrightarrow \left(if\left(x\in B,x,0_{ℎ}\right)=y{+}_{ℎ}z\to if\left(x\in B,x,0_{ℎ}\right)\in A\right)\right)$$
10		oveq1	$$⊢y=if\left(y\in A,y,0_{ℎ}\right)\to y{+}_{ℎ}z=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z$$
11	10	eqeq2d	$$⊢y=if\left(y\in A,y,0_{ℎ}\right)\to \left(if\left(x\in B,x,0_{ℎ}\right)=y{+}_{ℎ}z\leftrightarrow if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z\right)$$
12	11	imbi1d	$$⊢y=if\left(y\in A,y,0_{ℎ}\right)\to \left(\left(if\left(x\in B,x,0_{ℎ}\right)=y{+}_{ℎ}z\to if\left(x\in B,x,0_{ℎ}\right)\in A\right)\leftrightarrow \left(if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z\to if\left(x\in B,x,0_{ℎ}\right)\in A\right)\right)$$
13		oveq2	$$⊢z=if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\to if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)$$
14	13	eqeq2d	$$⊢z=if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\to \left(if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z\leftrightarrow if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\right)$$
15	14	imbi1d	$$⊢z=if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\to \left(\left(if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}z\to if\left(x\in B,x,0_{ℎ}\right)\in A\right)\leftrightarrow \left(if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\to if\left(x\in B,x,0_{ℎ}\right)\in A\right)\right)$$
16	1	chshii	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}$$
17		sh0	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in B$$
18	2 17	ax-mp	$$⊢0_{ℎ}\in B$$
19	18	elimel	$$⊢if\left(x\in B,x,0_{ℎ}\right)\in B$$
20		ch0	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}\to 0_{ℎ}\in A$$
21	1 20	ax-mp	$$⊢0_{ℎ}\in A$$
22	21	elimel	$$⊢if\left(y\in A,y,0_{ℎ}\right)\in A$$
23		shocsh	$$⊢A\in {\mathbf{S}}_{\mathscr{H}}\to \perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}$$
24	16 23	ax-mp	$$⊢\perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}$$
25		sh0	$$⊢\perp \left(A\right)\in {\mathbf{S}}_{\mathscr{H}}\to 0_{ℎ}\in \perp \left(A\right)$$
26	24 25	ax-mp	$$⊢0_{ℎ}\in \perp \left(A\right)$$
27	26	elimel	$$⊢if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\in \perp \left(A\right)$$
28	16 2 3 4 19 22 27	omlsilem	$$⊢if\left(x\in B,x,0_{ℎ}\right)=if\left(y\in A,y,0_{ℎ}\right){+}_{ℎ}if\left(z\in \perp \left(A\right),z,0_{ℎ}\right)\to if\left(x\in B,x,0_{ℎ}\right)\in A$$
29	9 12 15 28	dedth3h	$$⊢\left(x\in B\wedge y\in A\wedge z\in \perp \left(A\right)\right)\to \left(x=y{+}_{ℎ}z\to x\in A\right)$$
30	29	3expia	$$⊢\left(x\in B\wedge y\in A\right)\to \left(z\in \perp \left(A\right)\to \left(x=y{+}_{ℎ}z\to x\in A\right)\right)$$
31	30	rexlimdv	$$⊢\left(x\in B\wedge y\in A\right)\to \left(\exists z\in \perp \left(A\right)x=y{+}_{ℎ}z\to x\in A\right)$$
32	31	rexlimdva	$$⊢x\in B\to \left(\exists y\in A\exists z\in \perp \left(A\right)x=y{+}_{ℎ}z\to x\in A\right)$$
33	6 32	mpd	$$⊢x\in B\to x\in A$$
34	33	ssriv	$$⊢B\subseteq A$$
35	3 34	eqssi	$$⊢A=B$$