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 ⊢ 𝐴 ∈ Cℋ
qlaxr3.2 ⊢ 𝐵 ∈ Cℋ
qlaxr3.3 ⊢ 𝐶 ∈ Cℋ
qlaxr3.4 ⊢ ( 𝐶 ∨ℋ ( ⊥ ‘ 𝐶 ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
Assertion qlaxr3i 𝐴 = 𝐵

Proof

Step Hyp Ref Expression
1 qlaxr3.1 ⊢ 𝐴 ∈ Cℋ
2 qlaxr3.2 ⊢ 𝐵 ∈ Cℋ
3 qlaxr3.3 ⊢ 𝐶 ∈ Cℋ
4 qlaxr3.4 ⊢ ( 𝐶 ∨ℋ ( ⊥ ‘ 𝐶 ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
5 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
6 5 chshii ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Sℋ
7 1 2 chub1i ⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 )
8 incom ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) )
9 1 choccli ⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
10 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
11 1 2 cmj1i ⊢ 𝐴 𝐶ℋ ( 𝐴 ∨ℋ 𝐵 )
12 1 5 11 cmcmii ⊢ ( 𝐴 ∨ℋ 𝐵 ) 𝐶ℋ 𝐴
13 5 1 12 cmcm2ii ⊢ ( 𝐴 ∨ℋ 𝐵 ) 𝐶ℋ ( ⊥ ‘ 𝐴 )
14 1 2 cmj2i ⊢ 𝐵 𝐶ℋ ( 𝐴 ∨ℋ 𝐵 )
15 2 5 14 cmcmii ⊢ ( 𝐴 ∨ℋ 𝐵 ) 𝐶ℋ 𝐵
16 5 2 15 cmcm2ii ⊢ ( 𝐴 ∨ℋ 𝐵 ) 𝐶ℋ ( ⊥ ‘ 𝐵 )
17 5 9 10 13 16 fh1i ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) )
18 8 17 eqtr3i ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) )
19 3 chjoi ⊢ ( 𝐶 ∨ℋ ( ⊥ ‘ 𝐶 ) ) = ℋ
20 19 4 eqtr3i ⊢ ℋ = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
21 choc0 ⊢ ( ⊥ ‘ 0ℋ ) = ℋ
22 9 10 chjcli ⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
23 22 5 chdmm1i ⊢ ( ⊥ ‘ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∨ℋ ( ⊥ ‘ ( 𝐴 ∨ℋ 𝐵 ) ) )
24 20 21 23 3eqtr4i ⊢ ( ⊥ ‘ 0ℋ ) = ( ⊥ ‘ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) )
25 22 5 chincli ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ∈ Cℋ
26 h0elch ⊢ 0ℋ ∈ Cℋ
27 25 26 chcon3i ⊢ ( ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ ↔ ( ⊥ ‘ 0ℋ ) = ( ⊥ ‘ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
28 24 27 mpbir ⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ
29 18 28 eqtr3i ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = 0ℋ
30 5 9 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ Cℋ
31 5 10 chincli ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
32 30 31 chj00i ⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∧ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) = 0ℋ ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∨ℋ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) ) = 0ℋ )
33 29 32 mpbir ⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∧ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) = 0ℋ )
34 33 simpli ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ
35 1 6 7 34 omlsii ⊢ 𝐴 = ( 𝐴 ∨ℋ 𝐵 )
36 2 1 chub2i ⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 )
37 33 simpri ⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐵 ) ) = 0ℋ
38 2 6 36 37 omlsii ⊢ 𝐵 = ( 𝐴 ∨ℋ 𝐵 )
39 35 38 eqtr4i ⊢ 𝐴 = 𝐵