Metamath Proof Explorer

Theorem trlcnv

Description: The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013)

Ref Expression
Hypotheses trlcnv.h 
|- H = ( LHyp ` K )
trlcnv.t 
|- T = ( ( LTrn ` K ) ` W )
trlcnv.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlcnv 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )

Proof

Step Hyp Ref Expression
1 trlcnv.h 
 |-  H = ( LHyp ` K )
2 trlcnv.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 trlcnv.r 
 |-  R = ( ( trL ` K ) ` W )
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 4 5 1 lhpexnle 
 |-  ( ( K e. HL /\ W e. H ) -> E. p e. ( Atoms ` K ) -. p ( le ` K ) W )
7 6 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> E. p e. ( Atoms ` K ) -. p ( le ` K ) W )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
10 9 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
11 simp3l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> p e. ( Atoms ` K ) )
12 8 5 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. ( Base ` K ) )
13 11 12 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> p e. ( Base ` K ) )
14 f1ocnvfv1 
 |-  ( ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ p e. ( Base ` K ) ) -> ( `' F ` ( F ` p ) ) = p )
15 10 13 14 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( `' F ` ( F ` p ) ) = p )
16 15 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( F ` p ) ( join ` K ) ( `' F ` ( F ` p ) ) ) = ( ( F ` p ) ( join ` K ) p ) )
17 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> K e. HL )
18 4 5 1 2 ltrnat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ p e. ( Atoms ` K ) ) -> ( F ` p ) e. ( Atoms ` K ) )
19 18 3adant3r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( F ` p ) e. ( Atoms ` K ) )
20 eqid 
 |-  ( join ` K ) = ( join ` K )
21 20 5 hlatjcom 
 |-  ( ( K e. HL /\ ( F ` p ) e. ( Atoms ` K ) /\ p e. ( Atoms ` K ) ) -> ( ( F ` p ) ( join ` K ) p ) = ( p ( join ` K ) ( F ` p ) ) )
22 17 19 11 21 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( F ` p ) ( join ` K ) p ) = ( p ( join ` K ) ( F ` p ) ) )
23 16 22 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( F ` p ) ( join ` K ) ( `' F ` ( F ` p ) ) ) = ( p ( join ` K ) ( F ` p ) ) )
24 23 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( ( F ` p ) ( join ` K ) ( `' F ` ( F ` p ) ) ) ( meet ` K ) W ) = ( ( p ( join ` K ) ( F ` p ) ) ( meet ` K ) W ) )
25 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
26 1 2 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
27 26 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> `' F e. T )
28 4 5 1 2 ltrnel 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( ( F ` p ) e. ( Atoms ` K ) /\ -. ( F ` p ) ( le ` K ) W ) )
29 eqid 
 |-  ( meet ` K ) = ( meet ` K )
30 4 20 29 5 1 2 3 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ `' F e. T /\ ( ( F ` p ) e. ( Atoms ` K ) /\ -. ( F ` p ) ( le ` K ) W ) ) -> ( R ` `' F ) = ( ( ( F ` p ) ( join ` K ) ( `' F ` ( F ` p ) ) ) ( meet ` K ) W ) )
31 25 27 28 30 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` `' F ) = ( ( ( F ` p ) ( join ` K ) ( `' F ` ( F ` p ) ) ) ( meet ` K ) W ) )
32 4 20 29 5 1 2 3 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` F ) = ( ( p ( join ` K ) ( F ` p ) ) ( meet ` K ) W ) )
33 24 31 32 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` `' F ) = ( R ` F ) )
34 33 3expa 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( R ` `' F ) = ( R ` F ) )
35 7 34 rexlimddv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )