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 ( 𝐵𝐴 → ( 𝐴 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ 𝐵 ) ) = 𝐵 )