Metamath Proof Explorer

Theorem pjoml2

Description: Variation of orthomodular law. Definition in Kalmbach p. 22. (Contributed by NM, 13-Jun-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sseq1 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}\right)$
2 id ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to {A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)$
3 fveq2 ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \perp \left({A}\right)=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)$
4 3 ineq1d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \perp \left({A}\right)\cap {B}=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}$
5 2 4 oveq12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to {A}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap {B}\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)$
6 5 eqeq1d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left({A}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap {B}\right)={B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)={B}\right)$
7 1 6 imbi12d ${⊢}{A}=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\to \left(\left({A}\subseteq {B}\to {A}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap {B}\right)={B}\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)={B}\right)\right)$
8 sseq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
9 ineq2 ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}=\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
10 9 oveq2d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)=if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
11 id ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to {B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
12 10 11 eqeq12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)={B}↔if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)$
13 8 12 imbi12d ${⊢}{B}=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to \left(\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq {B}\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap {B}\right)={B}\right)↔\left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)\right)$
14 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
15 14 elimel ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
16 14 elimel ${⊢}if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
17 15 16 pjoml2i ${⊢}if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\subseteq if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\to if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right){\vee }_{ℋ}\left(\perp \left(if\left({A}\in {\mathbf{C}}_{ℋ},{A},{0}_{ℋ}\right)\right)\cap if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)\right)=if\left({B}\in {\mathbf{C}}_{ℋ},{B},{0}_{ℋ}\right)$
18 7 13 17 dedth2h ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {A}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap {B}\right)={B}\right)$
19 18 3impia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{\vee }_{ℋ}\left(\perp \left({A}\right)\cap {B}\right)={B}$