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 )