Metamath Proof Explorer

Theorem lvolex3N

Description: There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lvolex3.l ⊢ ≤ = ( le ‘ 𝐾 )
lvolex3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lvolex3.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lvolex3N ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 lvolex3.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvolex3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lvolex3.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6 4 1 5 2 3 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) ) )
7 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → 𝐾 ∈ HL )
8 simp1rl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → 𝑟 ∈ 𝐴 )
9 simp1rr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → 𝑠 ∈ 𝐴 )
10 simp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → 𝑡 ∈ 𝐴 )
11 5 1 2 3dim3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) )
12 7 8 9 10 11 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) )
13 simp33 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) )
14 breq2 ⊢ ( 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) → ( 𝑞 ≤ 𝑋 ↔ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) )
15 14 notbid ⊢ ( 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) → ( ¬ 𝑞 ≤ 𝑋 ↔ ¬ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) )
16 15 rexbidv ⊢ ( 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) → ( ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) )
17 13 16 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → ( ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ↔ ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) )
18 12 17 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) ∧ 𝑡 ∈ 𝐴 ∧ ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 )
19 18 rexlimdv3a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ) → ( ∃ 𝑡 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ) )
20 19 rexlimdvva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ) )
21 20 adantld ⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ( 𝑟 ≠ 𝑠 ∧ ¬ 𝑡 ≤ ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ∧ 𝑋 = ( ( 𝑟 ( join ‘ 𝐾 ) 𝑠 ) ( join ‘ 𝐾 ) 𝑡 ) ) ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ) )
22 6 21 sylbid ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑃 → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 ) )
23 22 imp ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑞 ∈ 𝐴 ¬ 𝑞 ≤ 𝑋 )