This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2lplnj

Description: The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012)

Ref Expression
Hypotheses 2lplnj.l 
|- .<_ = ( le ` K )
2lplnj.j 
|- .\/ = ( join ` K )
2lplnj.p 
|- P = ( LPlanes ` K )
2lplnj.v 
|- V = ( LVols ` K )
Assertion 2lplnj 
|- ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X .\/ Y ) = W )

Proof

Step Hyp Ref Expression
1 2lplnj.l 
 |-  .<_ = ( le ` K )
2 2lplnj.j 
 |-  .\/ = ( join ` K )
3 2lplnj.p 
 |-  P = ( LPlanes ` K )
4 2lplnj.v 
 |-  V = ( LVols ` K )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 5 1 2 6 3 islpln2 
 |-  ( K e. HL -> ( X e. P <-> ( X e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) ) )
8 simpr 
 |-  ( ( X e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) )
9 7 8 biimtrdi 
 |-  ( K e. HL -> ( X e. P -> E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) )
10 5 1 2 6 3 islpln2 
 |-  ( K e. HL -> ( Y e. P <-> ( Y e. ( Base ` K ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) ) )
11 simpr 
 |-  ( ( Y e. ( Base ` K ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) )
12 10 11 biimtrdi 
 |-  ( K e. HL -> ( Y e. P -> E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) )
13 9 12 anim12d 
 |-  ( K e. HL -> ( ( X e. P /\ Y e. P ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) ) )
14 13 imp 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) )
15 14 3adantr3 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) )
16 15 3adant3 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) )
17 simpl33 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> X = ( ( q .\/ r ) .\/ s ) )
18 17 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> X = ( ( q .\/ r ) .\/ s ) )
19 simp33 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> Y = ( ( t .\/ u ) .\/ v ) )
20 18 19 oveq12d 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( X .\/ Y ) = ( ( ( q .\/ r ) .\/ s ) .\/ ( ( t .\/ u ) .\/ v ) ) )
21 simp11 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> K e. HL )
22 simp123 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> W e. V )
23 21 22 jca 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> ( K e. HL /\ W e. V ) )
24 23 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> ( K e. HL /\ W e. V ) )
25 24 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( K e. HL /\ W e. V ) )
26 simp2l 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> q e. ( Atoms ` K ) )
27 simp2rl 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> r e. ( Atoms ` K ) )
28 simp2rr 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> s e. ( Atoms ` K ) )
29 26 27 28 3jca 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) )
30 29 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) )
31 30 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) )
32 simpl31 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> q =/= r )
33 32 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> q =/= r )
34 simpl32 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> -. s .<_ ( q .\/ r ) )
35 34 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> -. s .<_ ( q .\/ r ) )
36 33 35 jca 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( q =/= r /\ -. s .<_ ( q .\/ r ) ) )
37 simp1r 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> t e. ( Atoms ` K ) )
38 simp2l 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> u e. ( Atoms ` K ) )
39 simp2r 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> v e. ( Atoms ` K ) )
40 37 38 39 3jca 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) )
41 simp31 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> t =/= u )
42 simp32 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> -. v .<_ ( t .\/ u ) )
43 41 42 jca 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( t =/= u /\ -. v .<_ ( t .\/ u ) ) )
44 simpl13 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> ( X .<_ W /\ Y .<_ W /\ X =/= Y ) )
45 44 3ad2ant1 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( X .<_ W /\ Y .<_ W /\ X =/= Y ) )
46 breq1 
 |-  ( X = ( ( q .\/ r ) .\/ s ) -> ( X .<_ W <-> ( ( q .\/ r ) .\/ s ) .<_ W ) )
47 neeq1 
 |-  ( X = ( ( q .\/ r ) .\/ s ) -> ( X =/= Y <-> ( ( q .\/ r ) .\/ s ) =/= Y ) )
48 46 47 3anbi13d 
 |-  ( X = ( ( q .\/ r ) .\/ s ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( ( q .\/ r ) .\/ s ) .<_ W /\ Y .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= Y ) ) )
49 breq1 
 |-  ( Y = ( ( t .\/ u ) .\/ v ) -> ( Y .<_ W <-> ( ( t .\/ u ) .\/ v ) .<_ W ) )
50 neeq2 
 |-  ( Y = ( ( t .\/ u ) .\/ v ) -> ( ( ( q .\/ r ) .\/ s ) =/= Y <-> ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) )
51 49 50 3anbi23d 
 |-  ( Y = ( ( t .\/ u ) .\/ v ) -> ( ( ( ( q .\/ r ) .\/ s ) .<_ W /\ Y .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= Y ) <-> ( ( ( q .\/ r ) .\/ s ) .<_ W /\ ( ( t .\/ u ) .\/ v ) .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) ) )
52 48 51 sylan9bb 
 |-  ( ( X = ( ( q .\/ r ) .\/ s ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( ( q .\/ r ) .\/ s ) .<_ W /\ ( ( t .\/ u ) .\/ v ) .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) ) )
53 18 19 52 syl2anc 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( ( q .\/ r ) .\/ s ) .<_ W /\ ( ( t .\/ u ) .\/ v ) .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) ) )
54 45 53 mpbid 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( ( ( q .\/ r ) .\/ s ) .<_ W /\ ( ( t .\/ u ) .\/ v ) .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) )
55 1 2 6 4 2lplnja 
 |-  ( ( ( ( K e. HL /\ W e. V ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) ) ) /\ ( ( t e. ( Atoms ` K ) /\ u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) ) ) /\ ( ( ( q .\/ r ) .\/ s ) .<_ W /\ ( ( t .\/ u ) .\/ v ) .<_ W /\ ( ( q .\/ r ) .\/ s ) =/= ( ( t .\/ u ) .\/ v ) ) ) -> ( ( ( q .\/ r ) .\/ s ) .\/ ( ( t .\/ u ) .\/ v ) ) = W )
56 25 31 36 40 43 54 55 syl321anc 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( ( ( q .\/ r ) .\/ s ) .\/ ( ( t .\/ u ) .\/ v ) ) = W )
57 20 56 eqtrd 
 |-  ( ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) /\ ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) /\ ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( X .\/ Y ) = W )
58 57 3exp 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> ( ( u e. ( Atoms ` K ) /\ v e. ( Atoms ` K ) ) -> ( ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) ) )
59 58 rexlimdvv 
 |-  ( ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) /\ t e. ( Atoms ` K ) ) -> ( E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) )
60 59 rexlimdva 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) /\ ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) )
61 60 3exp 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( q e. ( Atoms ` K ) /\ ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) ) -> ( ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) ) ) )
62 61 expdimp 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ q e. ( Atoms ` K ) ) -> ( ( r e. ( Atoms ` K ) /\ s e. ( Atoms ` K ) ) -> ( ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) ) ) )
63 62 rexlimdvv 
 |-  ( ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ q e. ( Atoms ` K ) ) -> ( E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) ) )
64 63 rexlimdva 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) -> ( E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) -> ( X .\/ Y ) = W ) ) )
65 64 impd 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) E. s e. ( Atoms ` K ) ( q =/= r /\ -. s .<_ ( q .\/ r ) /\ X = ( ( q .\/ r ) .\/ s ) ) /\ E. t e. ( Atoms ` K ) E. u e. ( Atoms ` K ) E. v e. ( Atoms ` K ) ( t =/= u /\ -. v .<_ ( t .\/ u ) /\ Y = ( ( t .\/ u ) .\/ v ) ) ) -> ( X .\/ Y ) = W ) )
66 16 65 mpd 
 |-  ( ( K e. HL /\ ( X e. P /\ Y e. P /\ W e. V ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X .\/ Y ) = W )