This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lvoli3

Description: Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012)

Ref Expression
Hypotheses lvoli3.l ⊢ ≤ = ( le ‘ 𝐾 )
lvoli3.j ⊢ ∨ = ( join ‘ 𝐾 )
lvoli3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lvoli3.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
lvoli3.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvoli3 ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lvoli3.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvoli3.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lvoli3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lvoli3.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
5 lvoli3.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
6 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ 𝑃 )
7 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑄 ∈ 𝐴 )
8 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ¬ 𝑄 ≤ 𝑋 )
9 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) )
10 breq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑟 ≤ 𝑦 ↔ 𝑟 ≤ 𝑋 ) )
11 10 notbid ⊢ ( 𝑦 = 𝑋 → ( ¬ 𝑟 ≤ 𝑦 ↔ ¬ 𝑟 ≤ 𝑋 ) )
12 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∨ 𝑟 ) = ( 𝑋 ∨ 𝑟 ) )
13 12 eqeq2d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ↔ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) )
14 11 13 anbi12d ⊢ ( 𝑦 = 𝑋 → ( ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ↔ ( ¬ 𝑟 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) ) )
15 breq1 ⊢ ( 𝑟 = 𝑄 → ( 𝑟 ≤ 𝑋 ↔ 𝑄 ≤ 𝑋 ) )
16 15 notbid ⊢ ( 𝑟 = 𝑄 → ( ¬ 𝑟 ≤ 𝑋 ↔ ¬ 𝑄 ≤ 𝑋 ) )
17 oveq2 ⊢ ( 𝑟 = 𝑄 → ( 𝑋 ∨ 𝑟 ) = ( 𝑋 ∨ 𝑄 ) )
18 17 eqeq2d ⊢ ( 𝑟 = 𝑄 → ( ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ↔ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) )
19 16 18 anbi12d ⊢ ( 𝑟 = 𝑄 → ( ( ¬ 𝑟 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑟 ) ) ↔ ( ¬ 𝑄 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) ) )
20 14 19 rspc2ev ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ∧ ( ¬ 𝑄 ≤ 𝑋 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) ) ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) )
21 6 7 8 9 20 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) )
22 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝐾 ∈ HL )
23 22 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝐾 ∈ Lat )
24 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25 24 4 lplnbase ⊢ ( 𝑋 ∈ 𝑃 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
26 6 25 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
27 24 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
28 7 27 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
29 24 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
30 23 26 28 29 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
31 24 1 2 3 4 5 islvol3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ) )
32 22 30 31 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑟 ∈ 𝐴 ( ¬ 𝑟 ≤ 𝑦 ∧ ( 𝑋 ∨ 𝑄 ) = ( 𝑦 ∨ 𝑟 ) ) ) )
33 21 32 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴 ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) ∈ 𝑉 )