Metamath Proof Explorer

Theorem qlaxr3i

Description: A variation of the orthomodular law, showing CH is an orthomodular lattice. (This corresponds to axiom "ax-r3" in the Quantum Logic Explorer.) (Contributed by NM, 7-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses qlaxr3.1 
|- A e. CH
qlaxr3.2 
|- B e. CH
qlaxr3.3 
|- C e. CH
qlaxr3.4 
|- ( C vH ( _|_ ` C ) ) = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( A vH B ) ) )
Assertion qlaxr3i 
|- A = B

Proof

Step Hyp Ref Expression
1 qlaxr3.1 
 |-  A e. CH
2 qlaxr3.2 
 |-  B e. CH
3 qlaxr3.3 
 |-  C e. CH
4 qlaxr3.4 
 |-  ( C vH ( _|_ ` C ) ) = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( A vH B ) ) )
5 1 2 chjcli 
 |-  ( A vH B ) e. CH
6 5 chshii 
 |-  ( A vH B ) e. SH
7 1 2 chub1i 
 |-  A C_ ( A vH B )
8 incom 
 |-  ( ( A vH B ) i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) )
9 1 choccli 
 |-  ( _|_ ` A ) e. CH
10 2 choccli 
 |-  ( _|_ ` B ) e. CH
11 1 2 cmj1i 
 |-  A C_H ( A vH B )
12 1 5 11 cmcmii 
 |-  ( A vH B ) C_H A
13 5 1 12 cmcm2ii 
 |-  ( A vH B ) C_H ( _|_ ` A )
14 1 2 cmj2i 
 |-  B C_H ( A vH B )
15 2 5 14 cmcmii 
 |-  ( A vH B ) C_H B
16 5 2 15 cmcm2ii 
 |-  ( A vH B ) C_H ( _|_ ` B )
17 5 9 10 13 16 fh1i 
 |-  ( ( A vH B ) i^i ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) = ( ( ( A vH B ) i^i ( _|_ ` A ) ) vH ( ( A vH B ) i^i ( _|_ ` B ) ) )
18 8 17 eqtr3i 
 |-  ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) = ( ( ( A vH B ) i^i ( _|_ ` A ) ) vH ( ( A vH B ) i^i ( _|_ ` B ) ) )
19 3 chjoi 
 |-  ( C vH ( _|_ ` C ) ) = ~H
20 19 4 eqtr3i 
 |-  ~H = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( A vH B ) ) )
21 choc0 
 |-  ( _|_ ` 0H ) = ~H
22 9 10 chjcli 
 |-  ( ( _|_ ` A ) vH ( _|_ ` B ) ) e. CH
23 22 5 chdmm1i 
 |-  ( _|_ ` ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) ) = ( ( _|_ ` ( ( _|_ ` A ) vH ( _|_ ` B ) ) ) vH ( _|_ ` ( A vH B ) ) )
24 20 21 23 3eqtr4i 
 |-  ( _|_ ` 0H ) = ( _|_ ` ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) )
25 22 5 chincli 
 |-  ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) e. CH
26 h0elch 
 |-  0H e. CH
27 25 26 chcon3i 
 |-  ( ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) = 0H <-> ( _|_ ` 0H ) = ( _|_ ` ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) ) )
28 24 27 mpbir 
 |-  ( ( ( _|_ ` A ) vH ( _|_ ` B ) ) i^i ( A vH B ) ) = 0H
29 18 28 eqtr3i 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) vH ( ( A vH B ) i^i ( _|_ ` B ) ) ) = 0H
30 5 9 chincli 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) e. CH
31 5 10 chincli 
 |-  ( ( A vH B ) i^i ( _|_ ` B ) ) e. CH
32 30 31 chj00i 
 |-  ( ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H /\ ( ( A vH B ) i^i ( _|_ ` B ) ) = 0H ) <-> ( ( ( A vH B ) i^i ( _|_ ` A ) ) vH ( ( A vH B ) i^i ( _|_ ` B ) ) ) = 0H )
33 29 32 mpbir 
 |-  ( ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H /\ ( ( A vH B ) i^i ( _|_ ` B ) ) = 0H )
34 33 simpli 
 |-  ( ( A vH B ) i^i ( _|_ ` A ) ) = 0H
35 1 6 7 34 omlsii 
 |-  A = ( A vH B )
36 2 1 chub2i 
 |-  B C_ ( A vH B )
37 33 simpri 
 |-  ( ( A vH B ) i^i ( _|_ ` B ) ) = 0H
38 2 6 36 37 omlsii 
 |-  B = ( A vH B )
39 35 38 eqtr4i 
 |-  A = B