Theorem lvolbase

Description: A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	lvolbase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lvolbase.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion	lvolbase	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lvolbase.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lvolbase.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
3		n0i	⊢ ( 𝑋 ∈ 𝑉 → ¬ 𝑉 = ∅ )
4	2	eqeq1i	⊢ ( 𝑉 = ∅ ↔ ( LVols ‘ 𝐾 ) = ∅ )
5	3 4	sylnib	⊢ ( 𝑋 ∈ 𝑉 → ¬ ( LVols ‘ 𝐾 ) = ∅ )
6		fvprc	⊢ ( ¬ 𝐾 ∈ V → ( LVols ‘ 𝐾 ) = ∅ )
7	5 6	nsyl2	⊢ ( 𝑋 ∈ 𝑉 → 𝐾 ∈ V )
8		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
9		eqid	⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
10	1 8 9 2	islvol	⊢ ( 𝐾 ∈ V → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑥 ∈ ( LPlanes ‘ 𝐾 ) 𝑥 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
11	10	simprbda	⊢ ( ( 𝐾 ∈ V ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
12	7 11	mpancom	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐵 )