Metamath Proof Explorer

Theorem lvolnlelpln

Description: A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012)

Ref Expression
Hypotheses lvolnlelpln.l ⊢ ≤ = ( le ‘ 𝐾 )
lvolnlelpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
lvolnlelpln.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvolnlelpln ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑋 ≤ 𝑌 )

Proof

Step Hyp Ref Expression
1 lvolnlelpln.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvolnlelpln.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3 lvolnlelpln.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
4 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → 𝑌 ∈ 𝑃 )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
7 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 5 1 6 7 2 islpln2 ⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) ) )
9 8 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) ) )
10 4 9 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) )
11 simp1l1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝐾 ∈ HL )
12 simp1l2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝑋 ∈ 𝑉 )
13 simp1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) )
14 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) )
15 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) )
16 1 6 7 3 lvolnle3at ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ) → ¬ 𝑋 ≤ ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) )
17 11 12 13 14 15 16 syl23anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → ¬ 𝑋 ≤ ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) )
18 simp33 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) )
19 18 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 ≤ ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) )
20 17 19 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → ¬ 𝑋 ≤ 𝑌 )
21 20 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) → ¬ 𝑋 ≤ 𝑌 ) ) )
22 21 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) → ¬ 𝑋 ≤ 𝑌 ) )
23 22 rexlimdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) → ¬ 𝑋 ≤ 𝑌 ) )
24 23 adantld ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ ¬ 𝑠 ≤ ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ∧ 𝑌 = ( ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) ( join ‘ 𝐾 ) 𝑠 ) ) ) → ¬ 𝑋 ≤ 𝑌 ) )
25 10 24 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑋 ≤ 𝑌 )