Metamath Proof Explorer

Theorem ltrnideq

Description: Property of the identity lattice translation. (Contributed by NM, 27-May-2012)

Ref Expression
Hypotheses ltrnnidn.b 
|- B = ( Base ` K )
ltrnnidn.l 
|- .<_ = ( le ` K )
ltrnnidn.a 
|- A = ( Atoms ` K )
ltrnnidn.h 
|- H = ( LHyp ` K )
ltrnnidn.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion ltrnideq 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F = ( _I |` B ) <-> ( F ` P ) = P ) )

Proof

Step Hyp Ref Expression
1 ltrnnidn.b 
 |-  B = ( Base ` K )
2 ltrnnidn.l 
 |-  .<_ = ( le ` K )
3 ltrnnidn.a 
 |-  A = ( Atoms ` K )
4 ltrnnidn.h 
 |-  H = ( LHyp ` K )
5 ltrnnidn.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F = ( _I |` B ) ) -> F = ( _I |` B ) )
7 6 fveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F = ( _I |` B ) ) -> ( F ` P ) = ( ( _I |` B ) ` P ) )
8 simpl3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F = ( _I |` B ) ) -> P e. A )
9 1 3 atbase 
 |-  ( P e. A -> P e. B )
10 fvresi 
 |-  ( P e. B -> ( ( _I |` B ) ` P ) = P )
11 8 9 10 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F = ( _I |` B ) ) -> ( ( _I |` B ) ` P ) = P )
12 7 11 eqtrd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F = ( _I |` B ) ) -> ( F ` P ) = P )
13 12 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F = ( _I |` B ) -> ( F ` P ) = P ) )
14 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F =/= ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
15 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F =/= ( _I |` B ) ) -> F e. T )
16 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F =/= ( _I |` B ) ) -> F =/= ( _I |` B ) )
17 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F =/= ( _I |` B ) ) -> ( P e. A /\ -. P .<_ W ) )
18 1 2 3 4 5 ltrnnidn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) =/= P )
19 14 15 16 17 18 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ F =/= ( _I |` B ) ) -> ( F ` P ) =/= P )
20 19 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F =/= ( _I |` B ) -> ( F ` P ) =/= P ) )
21 20 necon4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) = P -> F = ( _I |` B ) ) )
22 13 21 impbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F = ( _I |` B ) <-> ( F ` P ) = P ) )