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

Metamath Proof Explorer

Theorem lvoli

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

Ref Expression
Hypotheses lvolset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lvolset.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lvolset.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
lvolset.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvoli ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 lvolset.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lvolset.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 lvolset.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 lvolset.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 simpl2 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝐵 )
6 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐶 𝑌 ↔ 𝑋 𝐶 𝑌 ) )
7 6 rspcev ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑥 ∈ 𝑃 𝑥 𝐶 𝑌 )
8 7 3ad2antl3 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → ∃ 𝑥 ∈ 𝑃 𝑥 𝐶 𝑌 )
9 simpl1 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → 𝐾 ∈ 𝐷 )
10 1 2 3 4 islvol ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑃 𝑥 𝐶 𝑌 ) ) )
11 9 10 syl ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑌 ∈ 𝑉 ↔ ( 𝑌 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝑃 𝑥 𝐶 𝑌 ) ) )
12 5 8 11 mpbir2and ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝑉 )