Metamath Proof Explorer

Theorem 3atnelvolN

Description: The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 3atnelvol.j ⊢ ∨ ˙ = join ⁡ K
3atnelvol.a ⊢ A = Atoms ⁡ K
3atnelvol.v ⊢ V = LVols ⁡ K
Assertion 3atnelvolN ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → ¬ P ∨ ˙ Q ∨ ˙ R ∈ V

Proof

Step Hyp Ref Expression
1 3atnelvol.j ⊢ ∨ ˙ = join ⁡ K
2 3atnelvol.a ⊢ A = Atoms ⁡ K
3 3atnelvol.v ⊢ V = LVols ⁡ K
4 hllat ⊢ K ∈ HL → K ∈ Lat
5 4 adantr ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → K ∈ Lat
6 eqid ⊢ Base K = Base K
7 6 1 2 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
8 7 3adant3r3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∈ Base K
9 simpr3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → R ∈ A
10 6 2 atbase ⊢ R ∈ A → R ∈ Base K
11 9 10 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → R ∈ Base K
12 6 1 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ R ∈ Base K → P ∨ ˙ Q ∨ ˙ R ∈ Base K
13 5 8 11 12 syl3anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R ∈ Base K
14 eqid ⊢ ≤ K = ≤ K
15 6 14 latref ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∨ ˙ R ∈ Base K → P ∨ ˙ Q ∨ ˙ R ≤ K P ∨ ˙ Q ∨ ˙ R
16 5 13 15 syl2anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R ≤ K P ∨ ˙ Q ∨ ˙ R
17 14 1 2 3 lvolnle3at ⊢ K ∈ HL ∧ P ∨ ˙ Q ∨ ˙ R ∈ V ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → ¬ P ∨ ˙ Q ∨ ˙ R ≤ K P ∨ ˙ Q ∨ ˙ R
18 17 an32s ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P ∨ ˙ Q ∨ ˙ R ∈ V → ¬ P ∨ ˙ Q ∨ ˙ R ≤ K P ∨ ˙ Q ∨ ˙ R
19 18 ex ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R ∈ V → ¬ P ∨ ˙ Q ∨ ˙ R ≤ K P ∨ ˙ Q ∨ ˙ R
20 16 19 mt2d ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → ¬ P ∨ ˙ Q ∨ ˙ R ∈ V