This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion pjoml4i ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∨ℋ 𝐵 )

Proof

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