Metamath Proof Explorer

Theorem islvol2aN

Description: The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses islvol2a.l 
|- .<_ = ( le ` K )
islvol2a.j 
|- .\/ = ( join ` K )
islvol2a.a 
|- A = ( Atoms ` K )
islvol2a.v 
|- V = ( LVols ` K )
Assertion islvol2aN 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) )

Proof

Step Hyp Ref Expression
1 islvol2a.l 
 |-  .<_ = ( le ` K )
2 islvol2a.j 
 |-  .\/ = ( join ` K )
3 islvol2a.a 
 |-  A = ( Atoms ` K )
4 islvol2a.v 
 |-  V = ( LVols ` K )
5 oveq1 
 |-  ( P = Q -> ( P .\/ Q ) = ( Q .\/ Q ) )
6 simpl1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> K e. HL )
7 simpl3 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> Q e. A )
8 2 3 hlatjidm 
 |-  ( ( K e. HL /\ Q e. A ) -> ( Q .\/ Q ) = Q )
9 6 7 8 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( Q .\/ Q ) = Q )
10 5 9 sylan9eqr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ P = Q ) -> ( P .\/ Q ) = Q )
11 10 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ P = Q ) -> ( ( P .\/ Q ) .\/ R ) = ( Q .\/ R ) )
12 11 oveq1d 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ P = Q ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( Q .\/ R ) .\/ S ) )
13 simprl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> R e. A )
14 simprr 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> S e. A )
15 2 3 4 3atnelvolN 
 |-  ( ( K e. HL /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> -. ( ( Q .\/ R ) .\/ S ) e. V )
16 6 7 13 14 15 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> -. ( ( Q .\/ R ) .\/ S ) e. V )
17 16 adantr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ P = Q ) -> -. ( ( Q .\/ R ) .\/ S ) e. V )
18 12 17 eqneltrd 
 |-  ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) /\ P = Q ) -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V )
19 18 ex 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( P = Q -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
20 19 necon2ad 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V -> P =/= Q ) )
21 6 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> K e. Lat )
22 eqid 
 |-  ( Base ` K ) = ( Base ` K )
23 22 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
24 23 ad2antrl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> R e. ( Base ` K ) )
25 22 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
26 25 adantr 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
27 22 1 2 latleeqj2 
 |-  ( ( K e. Lat /\ R e. ( Base ` K ) /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( R .<_ ( P .\/ Q ) <-> ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) ) )
28 21 24 26 27 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( R .<_ ( P .\/ Q ) <-> ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) ) )
29 simpl2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> P e. A )
30 2 3 4 3atnelvolN 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ S e. A ) ) -> -. ( ( P .\/ Q ) .\/ S ) e. V )
31 6 29 7 14 30 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> -. ( ( P .\/ Q ) .\/ S ) e. V )
32 oveq1 
 |-  ( ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ S ) )
33 32 eleq1d 
 |-  ( ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> ( ( P .\/ Q ) .\/ S ) e. V ) )
34 33 notbid 
 |-  ( ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) -> ( -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> -. ( ( P .\/ Q ) .\/ S ) e. V ) )
35 31 34 syl5ibrcom 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( P .\/ Q ) .\/ R ) = ( P .\/ Q ) -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
36 28 35 sylbid 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( R .<_ ( P .\/ Q ) -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
37 36 con2d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V -> -. R .<_ ( P .\/ Q ) ) )
38 22 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
39 38 ad2antll 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> S e. ( Base ` K ) )
40 22 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
41 21 26 24 40 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
42 22 1 2 latleeqj2 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) ) )
43 21 39 41 42 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) ) )
44 2 3 4 3atnelvolN 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> -. ( ( P .\/ Q ) .\/ R ) e. V )
45 6 29 7 13 44 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> -. ( ( P .\/ Q ) .\/ R ) e. V )
46 eleq1 
 |-  ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> ( ( P .\/ Q ) .\/ R ) e. V ) )
47 46 notbid 
 |-  ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) -> ( -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> -. ( ( P .\/ Q ) .\/ R ) e. V ) )
48 45 47 syl5ibrcom 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
49 43 48 sylbid 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) -> -. ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
50 49 con2d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V -> -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
51 20 37 50 3jcad 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V -> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) )
52 1 2 3 4 lvoli2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V )
53 52 3expia 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V ) )
54 51 53 impbid 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) )