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ℋ ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )