Theorem pjoml3

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	pjoml3	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B\subseteq A\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(B\subseteq A\leftrightarrow B\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
2		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)$$
3		fveq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
4	3	oveq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right){\vee }_{\mathscr{H}}B=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B$$
5	2 4	ineq12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)$$
6	5	eqeq1d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)=B\right)$$
7	1 6	imbi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(B\subseteq A\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=B\right)\leftrightarrow \left(B\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)=B\right)\right)$$
8		sseq1	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(B\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\leftrightarrow if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
9		oveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
10	9	ineq2d	$$⊢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 \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
11		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)$$
12	10 11	eqeq12d	$$⊢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)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)=B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
13	8 12	imbi12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(B\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}B\right)=B\right)\leftrightarrow \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\right)$$
14		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
15		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
16	14 15	pjoml3i	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\subseteq if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\cap \left(\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right){\vee }_{\mathscr{H}}if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)$$
17	7 13 16	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B\subseteq A\to A\cap \left(\perp \left(A\right){\vee }_{\mathscr{H}}B\right)=B\right)$$