Metamath Proof Explorer

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 ∈ C ℋ$
pjoml2.2 $⊢ B ∈ C ℋ$
Assertion pjoml2i $⊢ A ⊆ B → A ∨ ℋ ⊥ ⁡ A ∩ B = B$

Proof

Step Hyp Ref Expression
1 pjoml2.1 $⊢ A ∈ C ℋ$
2 pjoml2.2 $⊢ B ∈ C ℋ$
3 inss2 $⊢ ⊥ ⁡ A ∩ B ⊆ B$
4 1 choccli $⊢ ⊥ ⁡ A ∈ C ℋ$
5 4 2 chincli $⊢ ⊥ ⁡ A ∩ B ∈ C ℋ$
6 1 5 2 chlubii $⊢ A ⊆ B ∧ ⊥ ⁡ A ∩ B ⊆ B → A ∨ ℋ ⊥ ⁡ A ∩ B ⊆ B$
7 3 6 mpan2 $⊢ A ⊆ B → A ∨ ℋ ⊥ ⁡ A ∩ B ⊆ B$
8 1 5 chdmj1i $⊢ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ A ∩ B = ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B$
9 8 ineq2i $⊢ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ A ∩ B = B ∩ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B$
10 incom $⊢ B ∩ ⊥ ⁡ A = ⊥ ⁡ A ∩ B$
11 10 ineq1i $⊢ B ∩ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B = ⊥ ⁡ A ∩ B ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B$
12 inass $⊢ B ∩ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B = B ∩ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B$
13 5 chocini $⊢ ⊥ ⁡ A ∩ B ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B = 0 ℋ$
14 11 12 13 3eqtr3i $⊢ B ∩ ⊥ ⁡ A ∩ ⊥ ⁡ ⊥ ⁡ A ∩ B = 0 ℋ$
15 9 14 eqtri $⊢ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ A ∩ B = 0 ℋ$
16 1 5 chjcli $⊢ A ∨ ℋ ⊥ ⁡ A ∩ B ∈ C ℋ$
17 2 chshii $⊢ B ∈ S ℋ$
18 16 17 pjomli $⊢ A ∨ ℋ ⊥ ⁡ A ∩ B ⊆ B ∧ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ A ∩ B = 0 ℋ → A ∨ ℋ ⊥ ⁡ A ∩ B = B$
19 7 15 18 sylancl $⊢ A ⊆ B → A ∨ ℋ ⊥ ⁡ A ∩ B = B$