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