Metamath Proof Explorer

Theorem pjoml4i

Description: Variation of orthomodular law. (Contributed by NM, 6-Dec-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ A ∈ C ℋ
pjoml2.2 ⊢ B ∈ C ℋ
Assertion pjoml4i ⊢ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B = A ∨ ℋ B

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ A ∈ C ℋ
2 pjoml2.2 ⊢ B ∈ C ℋ
3 inss1 ⊢ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ B
4 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
5 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
6 4 5 chjcli ⊢ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∈ C ℋ
7 2 6 chincli ⊢ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∈ C ℋ
8 7 2 1 chlej2i ⊢ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ B → A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ A ∨ ℋ B
9 3 8 ax-mp ⊢ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ A ∨ ℋ B
10 1 7 chub1i ⊢ A ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
11 1 2 chdmm1i ⊢ ⊥ ⁡ A ∩ B = ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
12 11 ineq1i ⊢ ⊥ ⁡ A ∩ B ∩ B = ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∩ B
13 incom ⊢ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∩ B = B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
14 12 13 eqtri ⊢ ⊥ ⁡ A ∩ B ∩ B = B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
15 14 oveq2i ⊢ A ∩ B ∨ ℋ ⊥ ⁡ A ∩ B ∩ B = A ∩ B ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
16 inss2 ⊢ A ∩ B ⊆ B
17 1 2 chincli ⊢ A ∩ B ∈ C ℋ
18 17 2 pjoml2i ⊢ A ∩ B ⊆ B → A ∩ B ∨ ℋ ⊥ ⁡ A ∩ B ∩ B = B
19 16 18 ax-mp ⊢ A ∩ B ∨ ℋ ⊥ ⁡ A ∩ B ∩ B = B
20 15 19 eqtr3i ⊢ A ∩ B ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B = B
21 inss1 ⊢ A ∩ B ⊆ A
22 17 1 7 chlej1i ⊢ A ∩ B ⊆ A → A ∩ B ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
23 21 22 ax-mp ⊢ A ∩ B ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
24 20 23 eqsstrri ⊢ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
25 1 7 chjcli ⊢ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∈ C ℋ
26 1 2 25 chlubii ⊢ A ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B ∧ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B → A ∨ ℋ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
27 10 24 26 mp2an ⊢ A ∨ ℋ B ⊆ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B
28 9 27 eqssi ⊢ A ∨ ℋ B ∩ ⊥ ⁡ A ∨ ℋ ⊥ ⁡ B = A ∨ ℋ B