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