Metamath Proof Explorer

Theorem idltrn

Description: The identity function is a lattice translation. Remark below Lemma B in Crawley p. 112. (Contributed by NM, 18-May-2012)

Ref Expression
Hypotheses idltrn.b 
|- B = ( Base ` K )
idltrn.h 
|- H = ( LHyp ` K )
idltrn.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion idltrn 
|- ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )

Proof

Step Hyp Ref Expression
1 idltrn.b 
 |-  B = ( Base ` K )
2 idltrn.h 
 |-  H = ( LHyp ` K )
3 idltrn.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 eqid 
 |-  ( ( LDil ` K ) ` W ) = ( ( LDil ` K ) ` W )
5 1 2 4 idldil 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. ( ( LDil ` K ) ` W ) )
6 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( K e. HL /\ W e. H ) )
7 simplrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> q e. ( Atoms ` K ) )
8 simprr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> -. q ( le ` K ) W )
9 eqid 
 |-  ( le ` K ) = ( le ` K )
10 eqid 
 |-  ( meet ` K ) = ( meet ` K )
11 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
12 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
13 9 10 11 12 2 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( q e. ( Atoms ` K ) /\ -. q ( le ` K ) W ) ) -> ( q ( meet ` K ) W ) = ( 0. ` K ) )
14 6 7 8 13 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( q ( meet ` K ) W ) = ( 0. ` K ) )
15 1 12 atbase 
 |-  ( q e. ( Atoms ` K ) -> q e. B )
16 fvresi 
 |-  ( q e. B -> ( ( _I |` B ) ` q ) = q )
17 7 15 16 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( _I |` B ) ` q ) = q )
18 17 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( q ( join ` K ) ( ( _I |` B ) ` q ) ) = ( q ( join ` K ) q ) )
19 simplll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> K e. HL )
20 eqid 
 |-  ( join ` K ) = ( join ` K )
21 20 12 hlatjidm 
 |-  ( ( K e. HL /\ q e. ( Atoms ` K ) ) -> ( q ( join ` K ) q ) = q )
22 19 7 21 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( q ( join ` K ) q ) = q )
23 18 22 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( q ( join ` K ) ( ( _I |` B ) ` q ) ) = q )
24 23 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( q ( join ` K ) ( ( _I |` B ) ` q ) ) ( meet ` K ) W ) = ( q ( meet ` K ) W ) )
25 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> p e. ( Atoms ` K ) )
26 1 12 atbase 
 |-  ( p e. ( Atoms ` K ) -> p e. B )
27 fvresi 
 |-  ( p e. B -> ( ( _I |` B ) ` p ) = p )
28 25 26 27 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( _I |` B ) ` p ) = p )
29 28 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( p ( join ` K ) ( ( _I |` B ) ` p ) ) = ( p ( join ` K ) p ) )
30 20 12 hlatjidm 
 |-  ( ( K e. HL /\ p e. ( Atoms ` K ) ) -> ( p ( join ` K ) p ) = p )
31 19 25 30 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( p ( join ` K ) p ) = p )
32 29 31 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( p ( join ` K ) ( ( _I |` B ) ` p ) ) = p )
33 32 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( p ( meet ` K ) W ) )
34 simprl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> -. p ( le ` K ) W )
35 9 10 11 12 2 lhpmat 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ -. p ( le ` K ) W ) ) -> ( p ( meet ` K ) W ) = ( 0. ` K ) )
36 6 25 34 35 syl12anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( p ( meet ` K ) W ) = ( 0. ` K ) )
37 33 36 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( 0. ` K ) )
38 14 24 37 3eqtr4rd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) /\ ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( ( _I |` B ) ` q ) ) ( meet ` K ) W ) )
39 38 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. ( Atoms ` K ) /\ q e. ( Atoms ` K ) ) ) -> ( ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( ( _I |` B ) ` q ) ) ( meet ` K ) W ) ) )
40 39 ralrimivva 
 |-  ( ( K e. HL /\ W e. H ) -> A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) ( ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( ( _I |` B ) ` q ) ) ( meet ` K ) W ) ) )
41 9 20 10 12 2 4 3 isltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( _I |` B ) e. T <-> ( ( _I |` B ) e. ( ( LDil ` K ) ` W ) /\ A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) ( ( -. p ( le ` K ) W /\ -. q ( le ` K ) W ) -> ( ( p ( join ` K ) ( ( _I |` B ) ` p ) ) ( meet ` K ) W ) = ( ( q ( join ` K ) ( ( _I |` B ) ` q ) ) ( meet ` K ) W ) ) ) ) )
42 5 40 41 mpbir2and 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )