islvol3

Description: The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Hypotheses	islvol3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	islvol3.l	⊢ ≤ = ( le ‘ 𝐾 )
	islvol3.j	⊢ ∨ = ( join ‘ 𝐾 )
	islvol3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	islvol3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
	islvol3.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion	islvol3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		islvol3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		islvol3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		islvol3.j	⊢ ∨ = ( join ‘ 𝐾 )
4		islvol3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		islvol3.p	⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
6		islvol3.v	⊢ 𝑉 = ( LVols ‘ 𝐾 )
7		eqid	⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
8	1 7 5 6	islvol4	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
9		simpll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → 𝐾 ∈ HL )
10	1 5	lplnbase	⊢ ( 𝑦 ∈ 𝑃 → 𝑦 ∈ 𝐵 )
11	10	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑦 ∈ 𝐵 )
12		simplr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑋 ∈ 𝐵 )
13	1 2 3 7 4	cvrval3	⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ) )
14	9 11 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ) )
15		eqcom	⊢ ( ( 𝑦 ∨ 𝑝 ) = 𝑋 ↔ 𝑋 = ( 𝑦 ∨ 𝑝 ) )
16	15	a1i	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑦 ∨ 𝑝 ) = 𝑋 ↔ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) )
17	16	anbi2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ↔ ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
18	17	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ ( 𝑦 ∨ 𝑝 ) = 𝑋 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
19	14 18	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
20	19	rexbidva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑃 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )
21	8 20	bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = ( 𝑦 ∨ 𝑝 ) ) ) )

Metamath Proof Explorer

Theorem islvol3

Proof