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 ` K )
lvoli3.j
|- .\/ = ( join ` K )
lvoli3.a
|- A = ( Atoms ` K )
lvoli3.p
|- P = ( LPlanes ` K )
lvoli3.v
|- V = ( LVols ` K )
Assertion lvoli3
|- ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> ( X .\/ Q ) e. V )

Proof

Step Hyp Ref Expression
1 lvoli3.l
 |-  .<_ = ( le ` K )
2 lvoli3.j
 |-  .\/ = ( join ` K )
3 lvoli3.a
 |-  A = ( Atoms ` K )
4 lvoli3.p
 |-  P = ( LPlanes ` K )
5 lvoli3.v
 |-  V = ( LVols ` K )
6 simpl2
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> X e. P )
7 simpl3
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> Q e. A )
8 simpr
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> -. Q .<_ X )
9 eqidd
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> ( X .\/ Q ) = ( X .\/ Q ) )
10 breq2
 |-  ( y = X -> ( r .<_ y <-> r .<_ X ) )
11 10 notbid
 |-  ( y = X -> ( -. r .<_ y <-> -. r .<_ X ) )
12 oveq1
 |-  ( y = X -> ( y .\/ r ) = ( X .\/ r ) )
13 12 eqeq2d
 |-  ( y = X -> ( ( X .\/ Q ) = ( y .\/ r ) <-> ( X .\/ Q ) = ( X .\/ r ) ) )
14 11 13 anbi12d
 |-  ( y = X -> ( ( -. r .<_ y /\ ( X .\/ Q ) = ( y .\/ r ) ) <-> ( -. r .<_ X /\ ( X .\/ Q ) = ( X .\/ r ) ) ) )
15 breq1
 |-  ( r = Q -> ( r .<_ X <-> Q .<_ X ) )
16 15 notbid
 |-  ( r = Q -> ( -. r .<_ X <-> -. Q .<_ X ) )
17 oveq2
 |-  ( r = Q -> ( X .\/ r ) = ( X .\/ Q ) )
18 17 eqeq2d
 |-  ( r = Q -> ( ( X .\/ Q ) = ( X .\/ r ) <-> ( X .\/ Q ) = ( X .\/ Q ) ) )
19 16 18 anbi12d
 |-  ( r = Q -> ( ( -. r .<_ X /\ ( X .\/ Q ) = ( X .\/ r ) ) <-> ( -. Q .<_ X /\ ( X .\/ Q ) = ( X .\/ Q ) ) ) )
20 14 19 rspc2ev
 |-  ( ( X e. P /\ Q e. A /\ ( -. Q .<_ X /\ ( X .\/ Q ) = ( X .\/ Q ) ) ) -> E. y e. P E. r e. A ( -. r .<_ y /\ ( X .\/ Q ) = ( y .\/ r ) ) )
21 6 7 8 9 20 syl112anc
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> E. y e. P E. r e. A ( -. r .<_ y /\ ( X .\/ Q ) = ( y .\/ r ) ) )
22 simpl1
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> K e. HL )
23 22 hllatd
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> K e. Lat )
24 eqid
 |-  ( Base ` K ) = ( Base ` K )
25 24 4 lplnbase
 |-  ( X e. P -> X e. ( Base ` K ) )
26 6 25 syl
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> X e. ( Base ` K ) )
27 24 3 atbase
 |-  ( Q e. A -> Q e. ( Base ` K ) )
28 7 27 syl
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> Q e. ( Base ` K ) )
29 24 2 latjcl
 |-  ( ( K e. Lat /\ X e. ( Base ` K ) /\ Q e. ( Base ` K ) ) -> ( X .\/ Q ) e. ( Base ` K ) )
30 23 26 28 29 syl3anc
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> ( X .\/ Q ) e. ( Base ` K ) )
31 24 1 2 3 4 5 islvol3
 |-  ( ( K e. HL /\ ( X .\/ Q ) e. ( Base ` K ) ) -> ( ( X .\/ Q ) e. V <-> E. y e. P E. r e. A ( -. r .<_ y /\ ( X .\/ Q ) = ( y .\/ r ) ) ) )
32 22 30 31 syl2anc
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> ( ( X .\/ Q ) e. V <-> E. y e. P E. r e. A ( -. r .<_ y /\ ( X .\/ Q ) = ( y .\/ r ) ) ) )
33 21 32 mpbird
 |-  ( ( ( K e. HL /\ X e. P /\ Q e. A ) /\ -. Q .<_ X ) -> ( X .\/ Q ) e. V )