Metamath Proof Explorer

Theorem lvoli2

Description: The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012)

Ref Expression
Hypotheses lvoli2.l 
|- .<_ = ( le ` K )
lvoli2.j 
|- .\/ = ( join ` K )
lvoli2.a 
|- A = ( Atoms ` K )
lvoli2.v 
|- V = ( LVols ` K )
Assertion 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 )

Proof

Step Hyp Ref Expression
1 lvoli2.l 
 |-  .<_ = ( le ` K )
2 lvoli2.j 
 |-  .\/ = ( join ` K )
3 lvoli2.a 
 |-  A = ( Atoms ` K )
4 lvoli2.v 
 |-  V = ( LVols ` K )
5 simp12 
 |-  ( ( ( 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 e. A )
6 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. A )
7 simp3 
 |-  ( ( ( 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 .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
8 eqidd 
 |-  ( ( ( 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 ) = ( ( ( P .\/ Q ) .\/ R ) .\/ S ) )
9 neeq1 
 |-  ( p = P -> ( p =/= q <-> P =/= q ) )
10 oveq1 
 |-  ( p = P -> ( p .\/ q ) = ( P .\/ q ) )
11 10 breq2d 
 |-  ( p = P -> ( R .<_ ( p .\/ q ) <-> R .<_ ( P .\/ q ) ) )
12 11 notbid 
 |-  ( p = P -> ( -. R .<_ ( p .\/ q ) <-> -. R .<_ ( P .\/ q ) ) )
13 10 oveq1d 
 |-  ( p = P -> ( ( p .\/ q ) .\/ R ) = ( ( P .\/ q ) .\/ R ) )
14 13 breq2d 
 |-  ( p = P -> ( S .<_ ( ( p .\/ q ) .\/ R ) <-> S .<_ ( ( P .\/ q ) .\/ R ) ) )
15 14 notbid 
 |-  ( p = P -> ( -. S .<_ ( ( p .\/ q ) .\/ R ) <-> -. S .<_ ( ( P .\/ q ) .\/ R ) ) )
16 9 12 15 3anbi123d 
 |-  ( p = P -> ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) <-> ( P =/= q /\ -. R .<_ ( P .\/ q ) /\ -. S .<_ ( ( P .\/ q ) .\/ R ) ) ) )
17 13 oveq1d 
 |-  ( p = P -> ( ( ( p .\/ q ) .\/ R ) .\/ S ) = ( ( ( P .\/ q ) .\/ R ) .\/ S ) )
18 17 eqeq2d 
 |-  ( p = P -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ q ) .\/ R ) .\/ S ) ) )
19 16 18 anbi12d 
 |-  ( p = P -> ( ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) <-> ( ( P =/= q /\ -. R .<_ ( P .\/ q ) /\ -. S .<_ ( ( P .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ q ) .\/ R ) .\/ S ) ) ) )
20 neeq2 
 |-  ( q = Q -> ( P =/= q <-> P =/= Q ) )
21 oveq2 
 |-  ( q = Q -> ( P .\/ q ) = ( P .\/ Q ) )
22 21 breq2d 
 |-  ( q = Q -> ( R .<_ ( P .\/ q ) <-> R .<_ ( P .\/ Q ) ) )
23 22 notbid 
 |-  ( q = Q -> ( -. R .<_ ( P .\/ q ) <-> -. R .<_ ( P .\/ Q ) ) )
24 21 oveq1d 
 |-  ( q = Q -> ( ( P .\/ q ) .\/ R ) = ( ( P .\/ Q ) .\/ R ) )
25 24 breq2d 
 |-  ( q = Q -> ( S .<_ ( ( P .\/ q ) .\/ R ) <-> S .<_ ( ( P .\/ Q ) .\/ R ) ) )
26 25 notbid 
 |-  ( q = Q -> ( -. S .<_ ( ( P .\/ q ) .\/ R ) <-> -. S .<_ ( ( P .\/ Q ) .\/ R ) ) )
27 20 23 26 3anbi123d 
 |-  ( q = Q -> ( ( P =/= q /\ -. R .<_ ( P .\/ q ) /\ -. S .<_ ( ( P .\/ q ) .\/ R ) ) <-> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) )
28 24 oveq1d 
 |-  ( q = Q -> ( ( ( P .\/ q ) .\/ R ) .\/ S ) = ( ( ( P .\/ Q ) .\/ R ) .\/ S ) )
29 28 eqeq2d 
 |-  ( q = Q -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ q ) .\/ R ) .\/ S ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ Q ) .\/ R ) .\/ S ) ) )
30 27 29 anbi12d 
 |-  ( q = Q -> ( ( ( P =/= q /\ -. R .<_ ( P .\/ q ) /\ -. S .<_ ( ( P .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ q ) .\/ R ) .\/ S ) ) <-> ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ Q ) .\/ R ) .\/ S ) ) ) )
31 19 30 rspc2ev 
 |-  ( ( P e. A /\ Q e. A /\ ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( P .\/ Q ) .\/ R ) .\/ S ) ) ) -> E. p e. A E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) )
32 5 6 7 8 31 syl112anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> E. p e. A E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) )
33 32 3exp 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( R e. A /\ S e. A ) -> ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> E. p e. A E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) ) )
34 simplrl 
 |-  ( ( ( ( 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 ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) -> R e. A )
35 simplrr 
 |-  ( ( ( ( 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 ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) -> S e. A )
36 simpr 
 |-  ( ( ( ( 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 ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) -> ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) )
37 breq1 
 |-  ( r = R -> ( r .<_ ( p .\/ q ) <-> R .<_ ( p .\/ q ) ) )
38 37 notbid 
 |-  ( r = R -> ( -. r .<_ ( p .\/ q ) <-> -. R .<_ ( p .\/ q ) ) )
39 oveq2 
 |-  ( r = R -> ( ( p .\/ q ) .\/ r ) = ( ( p .\/ q ) .\/ R ) )
40 39 breq2d 
 |-  ( r = R -> ( s .<_ ( ( p .\/ q ) .\/ r ) <-> s .<_ ( ( p .\/ q ) .\/ R ) ) )
41 40 notbid 
 |-  ( r = R -> ( -. s .<_ ( ( p .\/ q ) .\/ r ) <-> -. s .<_ ( ( p .\/ q ) .\/ R ) ) )
42 38 41 3anbi23d 
 |-  ( r = R -> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ R ) ) ) )
43 39 oveq1d 
 |-  ( r = R -> ( ( ( p .\/ q ) .\/ r ) .\/ s ) = ( ( ( p .\/ q ) .\/ R ) .\/ s ) )
44 43 eqeq2d 
 |-  ( r = R -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ s ) ) )
45 42 44 anbi12d 
 |-  ( r = R -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ s ) ) ) )
46 breq1 
 |-  ( s = S -> ( s .<_ ( ( p .\/ q ) .\/ R ) <-> S .<_ ( ( p .\/ q ) .\/ R ) ) )
47 46 notbid 
 |-  ( s = S -> ( -. s .<_ ( ( p .\/ q ) .\/ R ) <-> -. S .<_ ( ( p .\/ q ) .\/ R ) ) )
48 47 3anbi3d 
 |-  ( s = S -> ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ R ) ) <-> ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) ) )
49 oveq2 
 |-  ( s = S -> ( ( ( p .\/ q ) .\/ R ) .\/ s ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) )
50 49 eqeq2d 
 |-  ( s = S -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ s ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) )
51 48 50 anbi12d 
 |-  ( s = S -> ( ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ s ) ) <-> ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) )
52 45 51 rspc2ev 
 |-  ( ( R e. A /\ S e. A /\ ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) -> E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
53 34 35 36 52 syl3anc 
 |-  ( ( ( ( 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 ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) ) -> E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
54 53 ex 
 |-  ( ( ( 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 ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) -> E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
55 54 reximdv 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) -> E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
56 55 reximdv 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( E. p e. A E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) -> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
57 56 ex 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( R e. A /\ S e. A ) -> ( E. p e. A E. q e. A ( ( p =/= q /\ -. R .<_ ( p .\/ q ) /\ -. S .<_ ( ( p .\/ q ) .\/ R ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ R ) .\/ S ) ) -> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
58 33 57 syldd 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( R e. A /\ S e. A ) -> ( ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) -> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
59 58 3imp 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
60 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. HL )
61 60 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. Lat )
62 eqid 
 |-  ( Base ` K ) = ( Base ` K )
63 62 2 3 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
64 63 3ad2ant1 
 |-  ( ( ( 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 ) e. ( Base ` K ) )
65 simp2l 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. A )
66 62 3 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
67 65 66 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. ( Base ` K ) )
68 62 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
69 61 64 67 68 syl3anc 
 |-  ( ( ( 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 ) e. ( Base ` K ) )
70 simp2r 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. A )
71 62 3 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
72 70 71 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) /\ ( P =/= Q /\ -. R .<_ ( P .\/ Q ) /\ -. S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. ( Base ` K ) )
73 62 2 latjcl 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) /\ S e. ( Base ` K ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. ( Base ` K ) )
74 61 69 72 73 syl3anc 
 |-  ( ( ( 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. ( Base ` K ) )
75 62 1 2 3 4 islvol5 
 |-  ( ( K e. HL /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. ( Base ` K ) ) -> ( ( ( ( P .\/ Q ) .\/ R ) .\/ S ) e. V <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
76 60 74 75 syl2anc 
 |-  ( ( ( 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 <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
77 59 76 mpbird 
 |-  ( ( ( 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 )