Metamath Proof Explorer

Theorem atexch

Description: The Hilbert lattice satisfies the atom exchange property. Proposition 1(i) of Kalmbach p. 140. A version of this theorem related to vector analysis was originally proved by Hermann Grassmann in 1862. Also Definition 3.4-3(b) in MegPav2000 p. 2345 (PDF p. 8) (use atnemeq0 to obtain atom inequality). (Contributed by NM, 27-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atexch 
|- ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> C C_ ( A vH B ) ) )

Proof

Step Hyp Ref Expression
1 atelch 
 |-  ( C e. HAtoms -> C e. CH )
2 chub2 
 |-  ( ( C e. CH /\ A e. CH ) -> C C_ ( A vH C ) )
3 2 ancoms 
 |-  ( ( A e. CH /\ C e. CH ) -> C C_ ( A vH C ) )
4 1 3 sylan2 
 |-  ( ( A e. CH /\ C e. HAtoms ) -> C C_ ( A vH C ) )
5 4 3adant2 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> C C_ ( A vH C ) )
6 5 adantr 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) ) -> C C_ ( A vH C ) )
7 cvp 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H <-> A
8 atelch 
 |-  ( B e. HAtoms -> B e. CH )
9 chjcl 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A vH B ) e. CH )
10 8 9 sylan2 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A vH B ) e. CH )
11 cvpss 
 |-  ( ( A e. CH /\ ( A vH B ) e. CH ) -> ( A  A C. ( A vH B ) ) )
12 10 11 syldan 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( A  A C. ( A vH B ) ) )
13 7 12 sylbid 
 |-  ( ( A e. CH /\ B e. HAtoms ) -> ( ( A i^i B ) = 0H -> A C. ( A vH B ) ) )
14 13 3adant3 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( A i^i B ) = 0H -> A C. ( A vH B ) ) )
15 14 adantld 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> A C. ( A vH B ) ) )
16 id 
 |-  ( A e. CH -> A e. CH )
17 chub1 
 |-  ( ( A e. CH /\ C e. CH ) -> A C_ ( A vH C ) )
18 17 3adant2 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> A C_ ( A vH C ) )
19 18 a1d 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B C_ ( A vH C ) -> A C_ ( A vH C ) ) )
20 19 ancrd 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B C_ ( A vH C ) -> ( A C_ ( A vH C ) /\ B C_ ( A vH C ) ) ) )
21 chjcl 
 |-  ( ( A e. CH /\ C e. CH ) -> ( A vH C ) e. CH )
22 21 3adant2 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A vH C ) e. CH )
23 chlub 
 |-  ( ( A e. CH /\ B e. CH /\ ( A vH C ) e. CH ) -> ( ( A C_ ( A vH C ) /\ B C_ ( A vH C ) ) <-> ( A vH B ) C_ ( A vH C ) ) )
24 22 23 syld3an3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( ( A C_ ( A vH C ) /\ B C_ ( A vH C ) ) <-> ( A vH B ) C_ ( A vH C ) ) )
25 20 24 sylibd 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( B C_ ( A vH C ) -> ( A vH B ) C_ ( A vH C ) ) )
26 16 8 1 25 syl3an 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( B C_ ( A vH C ) -> ( A vH B ) C_ ( A vH C ) ) )
27 26 adantrd 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> ( A vH B ) C_ ( A vH C ) ) )
28 15 27 jcad 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) ) )
29 28 imp 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) ) -> ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) )
30 simp1 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> A e. CH )
31 9 3adant3 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A vH B ) e. CH )
32 30 22 31 3jca 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A e. CH /\ ( A vH C ) e. CH /\ ( A vH B ) e. CH ) )
33 16 8 1 32 syl3an 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( A e. CH /\ ( A vH C ) e. CH /\ ( A vH B ) e. CH ) )
34 14 26 anim12d 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( ( A i^i B ) = 0H /\ B C_ ( A vH C ) ) -> ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) ) )
35 34 ancomsd 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) ) )
36 psssstr 
 |-  ( ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) -> A C. ( A vH C ) )
37 35 36 syl6 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> A C. ( A vH C ) ) )
38 chcv2 
 |-  ( ( A e. CH /\ C e. HAtoms ) -> ( A C. ( A vH C ) <-> A
39 38 3adant2 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( A C. ( A vH C ) <-> A
40 37 39 sylibd 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> A
41 cvnbtwn2 
 |-  ( ( A e. CH /\ ( A vH C ) e. CH /\ ( A vH B ) e. CH ) -> ( A  ( ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) -> ( A vH B ) = ( A vH C ) ) ) )
42 33 40 41 sylsyld 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> ( ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) -> ( A vH B ) = ( A vH C ) ) ) )
43 42 imp 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) ) -> ( ( A C. ( A vH B ) /\ ( A vH B ) C_ ( A vH C ) ) -> ( A vH B ) = ( A vH C ) ) )
44 29 43 mpd 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) ) -> ( A vH B ) = ( A vH C ) )
45 6 44 sseqtrrd 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) ) -> C C_ ( A vH B ) )
46 45 ex 
 |-  ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) -> ( ( B C_ ( A vH C ) /\ ( A i^i B ) = 0H ) -> C C_ ( A vH B ) ) )