Theorem pjoml2i

Description: Variation of orthomodular law. Definition in Kalmbach p. 22. (Contributed by NM, 31-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjoml2i	$$⊢A\subseteq B\to A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjoml2.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		inss2	$$⊢\perp \left(A\right)\cap B\subseteq B$$
4	1	choccli	$$⊢\perp \left(A\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 2	chincli	$$⊢\perp \left(A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
6	1 5 2	chlubii	$$⊢\left(A\subseteq B\wedge \perp \left(A\right)\cap B\subseteq B\right)\to A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\subseteq B$$
7	3 6	mpan2	$$⊢A\subseteq B\to A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\subseteq B$$
8	1 5	chdmj1i	$$⊢\perp \left(A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\right)=\perp \left(A\right)\cap \perp \left(\perp \left(A\right)\cap B\right)$$
9	8	ineq2i	$$⊢B\cap \perp \left(A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\right)=B\cap \left(\perp \left(A\right)\cap \perp \left(\perp \left(A\right)\cap B\right)\right)$$
10		incom	$$⊢B\cap \perp \left(A\right)=\perp \left(A\right)\cap B$$
11	10	ineq1i	$$⊢\left(B\cap \perp \left(A\right)\right)\cap \perp \left(\perp \left(A\right)\cap B\right)=\left(\perp \left(A\right)\cap B\right)\cap \perp \left(\perp \left(A\right)\cap B\right)$$
12		inass	$$⊢\left(B\cap \perp \left(A\right)\right)\cap \perp \left(\perp \left(A\right)\cap B\right)=B\cap \left(\perp \left(A\right)\cap \perp \left(\perp \left(A\right)\cap B\right)\right)$$
13	5	chocini	$$⊢\left(\perp \left(A\right)\cap B\right)\cap \perp \left(\perp \left(A\right)\cap B\right)=0_{\mathscr{H}}$$
14	11 12 13	3eqtr3i	$$⊢B\cap \left(\perp \left(A\right)\cap \perp \left(\perp \left(A\right)\cap B\right)\right)=0_{\mathscr{H}}$$
15	9 14	eqtri	$$⊢B\cap \perp \left(A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\right)=0_{\mathscr{H}}$$
16	1 5	chjcli	$$⊢A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\in {\mathbf{C}}_{\mathscr{H}}$$
17	2	chshii	$$⊢B\in {\mathbf{S}}_{\mathscr{H}}$$
18	16 17	pjomli	$$⊢\left(A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\subseteq B\wedge B\cap \perp \left(A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)\right)=0_{\mathscr{H}}\right)\to A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)=B$$
19	7 15 18	sylancl	$$⊢A\subseteq B\to A{\vee }_{\mathscr{H}}\left(\perp \left(A\right)\cap B\right)=B$$