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∈Cℋ
qlaxr3.2 ⊢B∈Cℋ
qlaxr3.3 ⊢C∈Cℋ
qlaxr3.4 ⊢C∨ℋ⊥⁡C=⊥⁡⊥⁡A∨ℋ⊥⁡B∨ℋ⊥⁡A∨ℋB
Assertion qlaxr3i ⊢A=B

Proof

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