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 ∈ C ℋ ∧ B ∈ HAtoms ∧ C ∈ HAtoms → B ⊆ A ∨ ℋ C ∧ A ∩ B = 0 ℋ → C ⊆ A ∨ ℋ B

Proof

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