Metamath Proof Explorer


Theorem atordi

Description: An ordering law for a Hilbert lattice atom and a commuting subspace. (Contributed by NM, 12-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 A C
Assertion atordi B HAtoms A 𝐶 B B A B A

Proof

Step Hyp Ref Expression
1 atoml.1 A C
2 atelch B HAtoms B C
3 1 choccli A C
4 chincl A C B C A B C
5 3 4 mpan B C A B C
6 chj0 A B C A B 0 = A B
7 5 6 syl B C A B 0 = A B
8 incom A B = B A
9 7 8 eqtrdi B C A B 0 = B A
10 h0elch 0 C
11 chjcom A B C 0 C A B 0 = 0 A B
12 5 10 11 sylancl B C A B 0 = 0 A B
13 9 12 eqtr3d B C B A = 0 A B
14 incom A A = A A
15 1 chocini A A = 0
16 14 15 eqtri A A = 0
17 16 oveq1i A A A B = 0 A B
18 13 17 eqtr4di B C B A = A A A B
19 18 adantr B C A 𝐶 B B A = A A A B
20 1 cmidi A 𝐶 A
21 1 1 20 cmcm2ii A 𝐶 A
22 fh2 A C A C B C A 𝐶 A A 𝐶 B A A B = A A A B
23 21 22 mpanr1 A C A C B C A 𝐶 B A A B = A A A B
24 1 23 mp3anl2 A C B C A 𝐶 B A A B = A A A B
25 3 24 mpanl1 B C A 𝐶 B A A B = A A A B
26 19 25 eqtr4d B C A 𝐶 B B A = A A B
27 2 26 sylan B HAtoms A 𝐶 B B A = A A B
28 incom A A B = A B A
29 27 28 eqtrdi B HAtoms A 𝐶 B B A = A B A
30 29 adantr B HAtoms A 𝐶 B ¬ B A B A = A B A
31 1 atoml2i B HAtoms ¬ B A A B A HAtoms
32 31 adantlr B HAtoms A 𝐶 B ¬ B A A B A HAtoms
33 30 32 eqeltrd B HAtoms A 𝐶 B ¬ B A B A HAtoms
34 atssma B HAtoms A C B A B A HAtoms
35 3 34 mpan2 B HAtoms B A B A HAtoms
36 35 ad2antrr B HAtoms A 𝐶 B ¬ B A B A B A HAtoms
37 33 36 mpbird B HAtoms A 𝐶 B ¬ B A B A
38 37 ex B HAtoms A 𝐶 B ¬ B A B A
39 38 orrd B HAtoms A 𝐶 B B A B A