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

Metamath Proof Explorer

Theorem pjoml3i

Description: Variation of orthomodular law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses pjoml2.1 ⊢ 𝐴 ∈ Cℋ
pjoml2.2 ⊢ 𝐵 ∈ Cℋ
Assertion pjoml3i ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 pjoml2.1 ⊢ 𝐴 ∈ Cℋ
2 pjoml2.2 ⊢ 𝐵 ∈ Cℋ
3 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
4 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
5 3 4 pjoml2i ⊢ ( ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝐵 ) → ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
6 2 1 chsscon3i ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( ⊥ ‘ 𝐴 ) ⊆ ( ⊥ ‘ 𝐵 ) )
7 eqcom ⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = 𝐵 ↔ 𝐵 = ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) )
8 3 choccli ⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ
9 8 4 chincli ⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
10 1 9 chdmj2i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) )
11 3 2 chdmm4i ⊢ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 )
12 11 ineq2i ⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
13 10 12 eqtri ⊢ ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) )
14 13 eqeq1i ⊢ ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) = 𝐵 ↔ ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )
15 3 9 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ
16 2 15 chcon2i ⊢ ( 𝐵 = ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) ) ↔ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
17 7 14 16 3bitr3i ⊢ ( ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 ↔ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ( ⊥ ‘ ( ⊥ ‘ 𝐴 ) ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ⊥ ‘ 𝐵 ) )
18 5 6 17 3imtr4i ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ 𝐵 ) ) = 𝐵 )