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

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

Proof

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