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 ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → 𝐶 ⊆ ( 𝐴 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 atelch ( 𝐶 ∈ HAtoms → 𝐶C )
2 chub2 ( ( 𝐶C𝐴C ) → 𝐶 ⊆ ( 𝐴 𝐶 ) )
3 2 ancoms ( ( 𝐴C𝐶C ) → 𝐶 ⊆ ( 𝐴 𝐶 ) )
4 1 3 sylan2 ( ( 𝐴C𝐶 ∈ HAtoms ) → 𝐶 ⊆ ( 𝐴 𝐶 ) )
5 4 3adant2 ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → 𝐶 ⊆ ( 𝐴 𝐶 ) )
6 5 adantr ( ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) ) → 𝐶 ⊆ ( 𝐴 𝐶 ) )
7 cvp ( ( 𝐴C𝐵 ∈ HAtoms ) → ( ( 𝐴𝐵 ) = 0𝐴 ( 𝐴 𝐵 ) ) )
8 atelch ( 𝐵 ∈ HAtoms → 𝐵C )
9 chjcl ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 ) ∈ C )
10 8 9 sylan2 ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 𝐵 ) ∈ C )
11 cvpss ( ( 𝐴C ∧ ( 𝐴 𝐵 ) ∈ C ) → ( 𝐴 ( 𝐴 𝐵 ) → 𝐴 ⊊ ( 𝐴 𝐵 ) ) )
12 10 11 syldan ( ( 𝐴C𝐵 ∈ HAtoms ) → ( 𝐴 ( 𝐴 𝐵 ) → 𝐴 ⊊ ( 𝐴 𝐵 ) ) )
13 7 12 sylbid ( ( 𝐴C𝐵 ∈ HAtoms ) → ( ( 𝐴𝐵 ) = 0𝐴 ⊊ ( 𝐴 𝐵 ) ) )
14 13 3adant3 ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴𝐵 ) = 0𝐴 ⊊ ( 𝐴 𝐵 ) ) )
15 14 adantld ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → 𝐴 ⊊ ( 𝐴 𝐵 ) ) )
16 id ( 𝐴C𝐴C )
17 chub1 ( ( 𝐴C𝐶C ) → 𝐴 ⊆ ( 𝐴 𝐶 ) )
18 17 3adant2 ( ( 𝐴C𝐵C𝐶C ) → 𝐴 ⊆ ( 𝐴 𝐶 ) )
19 18 a1d ( ( 𝐴C𝐵C𝐶C ) → ( 𝐵 ⊆ ( 𝐴 𝐶 ) → 𝐴 ⊆ ( 𝐴 𝐶 ) ) )
20 19 ancrd ( ( 𝐴C𝐵C𝐶C ) → ( 𝐵 ⊆ ( 𝐴 𝐶 ) → ( 𝐴 ⊆ ( 𝐴 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 𝐶 ) ) ) )
21 chjcl ( ( 𝐴C𝐶C ) → ( 𝐴 𝐶 ) ∈ C )
22 21 3adant2 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐶 ) ∈ C )
23 chlub ( ( 𝐴C𝐵C ∧ ( 𝐴 𝐶 ) ∈ C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 𝐶 ) ) ↔ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
24 22 23 syld3an3 ( ( 𝐴C𝐵C𝐶C ) → ( ( 𝐴 ⊆ ( 𝐴 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 𝐶 ) ) ↔ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
25 20 24 sylibd ( ( 𝐴C𝐵C𝐶C ) → ( 𝐵 ⊆ ( 𝐴 𝐶 ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
26 16 8 1 25 syl3an ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 ⊆ ( 𝐴 𝐶 ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
27 26 adantrd ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
28 15 27 jcad ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) ) )
29 28 imp ( ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) ) → ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) )
30 simp1 ( ( 𝐴C𝐵C𝐶C ) → 𝐴C )
31 9 3adant3 ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴 𝐵 ) ∈ C )
32 30 22 31 3jca ( ( 𝐴C𝐵C𝐶C ) → ( 𝐴C ∧ ( 𝐴 𝐶 ) ∈ C ∧ ( 𝐴 𝐵 ) ∈ C ) )
33 16 8 1 32 syl3an ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴C ∧ ( 𝐴 𝐶 ) ∈ C ∧ ( 𝐴 𝐵 ) ∈ C ) )
34 14 26 anim12d ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( 𝐴𝐵 ) = 0𝐵 ⊆ ( 𝐴 𝐶 ) ) → ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) ) )
35 34 ancomsd ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) ) )
36 psssstr ( ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) → 𝐴 ⊊ ( 𝐴 𝐶 ) )
37 35 36 syl6 ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → 𝐴 ⊊ ( 𝐴 𝐶 ) ) )
38 chcv2 ( ( 𝐴C𝐶 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐴 𝐶 ) ↔ 𝐴 ( 𝐴 𝐶 ) ) )
39 38 3adant2 ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐴 𝐶 ) ↔ 𝐴 ( 𝐴 𝐶 ) ) )
40 37 39 sylibd ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → 𝐴 ( 𝐴 𝐶 ) ) )
41 cvnbtwn2 ( ( 𝐴C ∧ ( 𝐴 𝐶 ) ∈ C ∧ ( 𝐴 𝐵 ) ∈ C ) → ( 𝐴 ( 𝐴 𝐶 ) → ( ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) → ( 𝐴 𝐵 ) = ( 𝐴 𝐶 ) ) ) )
42 33 40 41 sylsyld ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → ( ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) → ( 𝐴 𝐵 ) = ( 𝐴 𝐶 ) ) ) )
43 42 imp ( ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) ) → ( ( 𝐴 ⊊ ( 𝐴 𝐵 ) ∧ ( 𝐴 𝐵 ) ⊆ ( 𝐴 𝐶 ) ) → ( 𝐴 𝐵 ) = ( 𝐴 𝐶 ) ) )
44 29 43 mpd ( ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) ) → ( 𝐴 𝐵 ) = ( 𝐴 𝐶 ) )
45 6 44 sseqtrrd ( ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) ) → 𝐶 ⊆ ( 𝐴 𝐵 ) )
46 45 ex ( ( 𝐴C𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 𝐶 ) ∧ ( 𝐴𝐵 ) = 0 ) → 𝐶 ⊆ ( 𝐴 𝐵 ) ) )