Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trlval3 Structured version   Unicode version

Theorem trlval3 33553
Description: The value of the trace of a lattice translation in terms of 2 atoms. TODO: Try to shorten proof. (Contributed by NM, 3-May-2013.)
Hypotheses
Ref Expression
trlval3.l  |-  .<_  =  ( le `  K )
trlval3.j  |-  .\/  =  ( join `  K )
trlval3.m  |-  ./\  =  ( meet `  K )
trlval3.a  |-  A  =  ( Atoms `  K )
trlval3.h  |-  H  =  ( LHyp `  K
)
trlval3.t  |-  T  =  ( ( LTrn `  K
) `  W )
trlval3.r  |-  R  =  ( ( trL `  K
) `  W )
Assertion
Ref Expression
trlval3  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  ( Q  .\/  ( F `  Q
) ) ) )

Proof of Theorem trlval3
StepHypRef Expression
1 simpl1 986 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( K  e.  HL  /\  W  e.  H ) )
2 simpl31 1064 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
3 simpl2 987 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  ->  F  e.  T )
4 simpr 458 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( F `  P
)  =  P )
5 trlval3.l . . . . 5  |-  .<_  =  ( le `  K )
6 eqid 2441 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 trlval3.a . . . . 5  |-  A  =  ( Atoms `  K )
8 trlval3.h . . . . 5  |-  H  =  ( LHyp `  K
)
9 trlval3.t . . . . 5  |-  T  =  ( ( LTrn `  K
) `  W )
10 trlval3.r . . . . 5  |-  R  =  ( ( trL `  K
) `  W )
115, 6, 7, 8, 9, 10trl0 33536 . . . 4  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F  e.  T  /\  ( F `  P )  =  P ) )  ->  ( R `  F )  =  ( 0. `  K ) )
121, 2, 3, 4, 11syl112anc 1217 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( R `  F
)  =  ( 0.
`  K ) )
13 simpl33 1066 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  .\/  ( F `  P )
)  =/=  ( Q 
.\/  ( F `  Q ) ) )
14 simpl1l 1034 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  ->  K  e.  HL )
15 hlatl 32727 . . . . . 6  |-  ( K  e.  HL  ->  K  e.  AtLat )
1614, 15syl 16 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  ->  K  e.  AtLat )
174oveq2d 6106 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  .\/  ( F `  P )
)  =  ( P 
.\/  P ) )
18 simp31l 1106 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  P  e.  A )
1918adantr 462 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  ->  P  e.  A )
20 trlval3.j . . . . . . . . 9  |-  .\/  =  ( join `  K )
2120, 7hlatjidm 32735 . . . . . . . 8  |-  ( ( K  e.  HL  /\  P  e.  A )  ->  ( P  .\/  P
)  =  P )
2214, 19, 21syl2anc 656 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  .\/  P
)  =  P )
2317, 22eqtrd 2473 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  .\/  ( F `  P )
)  =  P )
2423, 19eqeltrd 2515 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( P  .\/  ( F `  P )
)  e.  A )
25 simp1 983 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( K  e.  HL  /\  W  e.  H ) )
26 simp2 984 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  F  e.  T )
27 simp31 1019 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( P  e.  A  /\  -.  P  .<_  W ) )
28 simp32 1020 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( Q  e.  A  /\  -.  Q  .<_  W ) )
295, 7, 8, 9ltrn2ateq 33546 . . . . . . . . . 10  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) ) )  ->  (
( F `  P
)  =  P  <->  ( F `  Q )  =  Q ) )
3025, 26, 27, 28, 29syl13anc 1215 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( ( F `  P )  =  P  <->  ( F `  Q )  =  Q ) )
3130biimpa 481 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( F `  Q
)  =  Q )
3231oveq2d 6106 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( Q  .\/  ( F `  Q )
)  =  ( Q 
.\/  Q ) )
33 simp32l 1108 . . . . . . . . 9  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  Q  e.  A )
3433adantr 462 . . . . . . . 8  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  ->  Q  e.  A )
3520, 7hlatjidm 32735 . . . . . . . 8  |-  ( ( K  e.  HL  /\  Q  e.  A )  ->  ( Q  .\/  Q
)  =  Q )
3614, 34, 35syl2anc 656 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( Q  .\/  Q
)  =  Q )
3732, 36eqtrd 2473 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( Q  .\/  ( F `  Q )
)  =  Q )
3837, 34eqeltrd 2515 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( Q  .\/  ( F `  Q )
)  e.  A )
39 trlval3.m . . . . . 6  |-  ./\  =  ( meet `  K )
4039, 6, 7atnem0 32685 . . . . 5  |-  ( ( K  e.  AtLat  /\  ( P  .\/  ( F `  P ) )  e.  A  /\  ( Q 
.\/  ( F `  Q ) )  e.  A )  ->  (
( P  .\/  ( F `  P )
)  =/=  ( Q 
.\/  ( F `  Q ) )  <->  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  =  ( 0.
`  K ) ) )
4116, 24, 38, 40syl3anc 1213 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) )  <->  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  =  ( 0.
`  K ) ) )
4213, 41mpbid 210 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =  ( 0. `  K
) )
4312, 42eqtr4d 2476 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =  P )  -> 
( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  ( Q  .\/  ( F `  Q ) ) ) )
44 simpl1 986 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( K  e.  HL  /\  W  e.  H ) )
45 simpl2 987 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  F  e.  T )
46 simpl31 1064 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( P  e.  A  /\  -.  P  .<_  W ) )
475, 20, 39, 7, 8, 9, 10trlval2 33529 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( P  e.  A  /\  -.  P  .<_  W ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  W )
)
4844, 45, 46, 47syl3anc 1213 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  W ) )
49 simpl1l 1034 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  K  e.  HL )
50 hllat 32730 . . . . . . 7  |-  ( K  e.  HL  ->  K  e.  Lat )
5149, 50syl 16 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  K  e.  Lat )
5218adantr 462 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  P  e.  A )
535, 7, 8, 9ltrnat 33506 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  P  e.  A
)  ->  ( F `  P )  e.  A
)
5444, 45, 52, 53syl3anc 1213 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( F `  P
)  e.  A )
55 eqid 2441 . . . . . . . 8  |-  ( Base `  K )  =  (
Base `  K )
5655, 20, 7hlatjcl 32733 . . . . . . 7  |-  ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
5749, 52, 54, 56syl3anc 1213 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( P  .\/  ( F `  P )
)  e.  ( Base `  K ) )
58 simpl1r 1035 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  W  e.  H )
5955, 8lhpbase 33364 . . . . . . 7  |-  ( W  e.  H  ->  W  e.  ( Base `  K
) )
6058, 59syl 16 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  W  e.  ( Base `  K ) )
6155, 5, 39latmle1 15242 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( P  .\/  ( F `  P ) )  ./\  W )  .<_  ( P  .\/  ( F `  P
) ) )
6251, 57, 60, 61syl3anc 1213 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( P  .\/  ( F `  P ) )  ./\  W )  .<_  ( P  .\/  ( F `  P )
) )
6348, 62eqbrtrd 4309 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  .<_  ( P  .\/  ( F `  P ) ) )
64 simpl32 1065 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( Q  e.  A  /\  -.  Q  .<_  W ) )
655, 20, 39, 7, 8, 9, 10trlval2 33529 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( Q  e.  A  /\  -.  Q  .<_  W ) )  ->  ( R `  F )  =  ( ( Q  .\/  ( F `  Q )
)  ./\  W )
)
6644, 45, 64, 65syl3anc 1213 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  =  ( ( Q  .\/  ( F `
 Q ) ) 
./\  W ) )
6733adantr 462 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  Q  e.  A )
685, 7, 8, 9ltrnat 33506 . . . . . . . 8  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  Q  e.  A
)  ->  ( F `  Q )  e.  A
)
6944, 45, 67, 68syl3anc 1213 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( F `  Q
)  e.  A )
7055, 20, 7hlatjcl 32733 . . . . . . 7  |-  ( ( K  e.  HL  /\  Q  e.  A  /\  ( F `  Q )  e.  A )  -> 
( Q  .\/  ( F `  Q )
)  e.  ( Base `  K ) )
7149, 67, 69, 70syl3anc 1213 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( Q  .\/  ( F `  Q )
)  e.  ( Base `  K ) )
7255, 5, 39latmle1 15242 . . . . . 6  |-  ( ( K  e.  Lat  /\  ( Q  .\/  ( F `
 Q ) )  e.  ( Base `  K
)  /\  W  e.  ( Base `  K )
)  ->  ( ( Q  .\/  ( F `  Q ) )  ./\  W )  .<_  ( Q  .\/  ( F `  Q
) ) )
7351, 71, 60, 72syl3anc 1213 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( Q  .\/  ( F `  Q ) )  ./\  W )  .<_  ( Q  .\/  ( F `  Q )
) )
7466, 73eqbrtrd 4309 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  .<_  ( Q  .\/  ( F `  Q ) ) )
7555, 8, 9, 10trlcl 33530 . . . . . 6  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T
)  ->  ( R `  F )  e.  (
Base `  K )
)
7644, 45, 75syl2anc 656 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  e.  ( Base `  K ) )
7755, 5, 39latlem12 15244 . . . . 5  |-  ( ( K  e.  Lat  /\  ( ( R `  F )  e.  (
Base `  K )  /\  ( P  .\/  ( F `  P )
)  e.  ( Base `  K )  /\  ( Q  .\/  ( F `  Q ) )  e.  ( Base `  K
) ) )  -> 
( ( ( R `
 F )  .<_  ( P  .\/  ( F `
 P ) )  /\  ( R `  F )  .<_  ( Q 
.\/  ( F `  Q ) ) )  <-> 
( R `  F
)  .<_  ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) ) ) )
7851, 76, 57, 71, 77syl13anc 1215 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( ( R `
 F )  .<_  ( P  .\/  ( F `
 P ) )  /\  ( R `  F )  .<_  ( Q 
.\/  ( F `  Q ) ) )  <-> 
( R `  F
)  .<_  ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) ) ) )
7963, 74, 78mpbi2and 907 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  .<_  ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) ) )
8049, 15syl 16 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  K  e.  AtLat )
81 simpr 458 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( F `  P
)  =/=  P )
825, 7, 8, 9, 10trlat 33535 . . . . 5  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  ( P  e.  A  /\  -.  P  .<_  W )  /\  ( F  e.  T  /\  ( F `  P )  =/=  P ) )  ->  ( R `  F )  e.  A
)
8344, 46, 45, 81, 82syl112anc 1217 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  e.  A )
8455, 39latmcl 15218 . . . . . . . 8  |-  ( ( K  e.  Lat  /\  ( P  .\/  ( F `
 P ) )  e.  ( Base `  K
)  /\  ( Q  .\/  ( F `  Q
) )  e.  (
Base `  K )
)  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  e.  ( Base `  K ) )
8551, 57, 71, 84syl3anc 1213 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  e.  ( Base `  K
) )
8655, 5, 6, 7atlen0 32677 . . . . . . 7  |-  ( ( ( K  e.  AtLat  /\  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  e.  ( Base `  K
)  /\  ( R `  F )  e.  A
)  /\  ( R `  F )  .<_  ( ( P  .\/  ( F `
 P ) ) 
./\  ( Q  .\/  ( F `  Q ) ) ) )  -> 
( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =/=  ( 0. `  K
) )
8780, 85, 83, 79, 86syl31anc 1216 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =/=  ( 0. `  K
) )
8887neneqd 2622 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  ->  -.  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =  ( 0. `  K
) )
89 simpl33 1066 . . . . . . 7  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( P  .\/  ( F `  P )
)  =/=  ( Q 
.\/  ( F `  Q ) ) )
9020, 39, 6, 72atmat0 32892 . . . . . . 7  |-  ( ( ( K  e.  HL  /\  P  e.  A  /\  ( F `  P )  e.  A )  /\  ( Q  e.  A  /\  ( F `  Q
)  e.  A  /\  ( P  .\/  ( F `
 P ) )  =/=  ( Q  .\/  ( F `  Q ) ) ) )  -> 
( ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  e.  A  \/  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =  ( 0. `  K
) ) )
9149, 52, 54, 67, 69, 89, 90syl33anc 1228 . . . . . 6  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  e.  A  \/  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =  ( 0. `  K
) ) )
9291ord 377 . . . . 5  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( -.  ( ( P  .\/  ( F `
 P ) ) 
./\  ( Q  .\/  ( F `  Q ) ) )  e.  A  ->  ( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  =  ( 0. `  K
) ) )
9388, 92mt3d 125 . . . 4  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( P  .\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `  Q
) ) )  e.  A )
945, 7atcmp 32678 . . . 4  |-  ( ( K  e.  AtLat  /\  ( R `  F )  e.  A  /\  (
( P  .\/  ( F `  P )
)  ./\  ( Q  .\/  ( F `  Q
) ) )  e.  A )  ->  (
( R `  F
)  .<_  ( ( P 
.\/  ( F `  P ) )  ./\  ( Q  .\/  ( F `
 Q ) ) )  <->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  ( Q  .\/  ( F `  Q
) ) ) ) )
9580, 83, 93, 94syl3anc 1213 . . 3  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( ( R `  F )  .<_  ( ( P  .\/  ( F `
 P ) ) 
./\  ( Q  .\/  ( F `  Q ) ) )  <->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  ( Q  .\/  ( F `  Q
) ) ) ) )
9679, 95mpbid 210 . 2  |-  ( ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  (
( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q  .\/  ( F `  Q )
) ) )  /\  ( F `  P )  =/=  P )  -> 
( R `  F
)  =  ( ( P  .\/  ( F `
 P ) ) 
./\  ( Q  .\/  ( F `  Q ) ) ) )
9743, 96pm2.61dane 2687 1  |-  ( ( ( K  e.  HL  /\  W  e.  H )  /\  F  e.  T  /\  ( ( P  e.  A  /\  -.  P  .<_  W )  /\  ( Q  e.  A  /\  -.  Q  .<_  W )  /\  ( P  .\/  ( F `  P ) )  =/=  ( Q 
.\/  ( F `  Q ) ) ) )  ->  ( R `  F )  =  ( ( P  .\/  ( F `  P )
)  ./\  ( Q  .\/  ( F `  Q
) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1761    =/= wne 2604   class class class wbr 4289   ` cfv 5415  (class class class)co 6090   Basecbs 14170   lecple 14241   joincjn 15110   meetcmee 15111   0.cp0 15203   Latclat 15211   Atomscatm 32630   AtLatcal 32631   HLchlt 32717   LHypclh 33350   LTrncltrn 33467   trLctrl 33524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-map 7212  df-poset 15112  df-plt 15124  df-lub 15140  df-glb 15141  df-join 15142  df-meet 15143  df-p0 15205  df-p1 15206  df-lat 15212  df-clat 15274  df-oposet 32543  df-ol 32545  df-oml 32546  df-covers 32633  df-ats 32634  df-atl 32665  df-cvlat 32689  df-hlat 32718  df-llines 32864  df-lhyp 33354  df-laut 33355  df-ldil 33470  df-ltrn 33471  df-trl 33525
This theorem is referenced by:  trlval4  33554
  Copyright terms: Public domain W3C validator