Metamath Proof Explorer

Theorem ltrneq3

Description: Two translations agree at any atom not under the fiducial co-atom W iff they are equal. (Contributed by NM, 25-Jul-2013)

Ref Expression
Hypotheses cdlemd.l 
|- .<_ = ( le ` K )
cdlemd.a 
|- A = ( Atoms ` K )
cdlemd.h 
|- H = ( LHyp ` K )
cdlemd.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion ltrneq3 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) = ( G ` P ) <-> F = G ) )

Proof

Step Hyp Ref Expression
1 cdlemd.l 
 |-  .<_ = ( le ` K )
2 cdlemd.a 
 |-  A = ( Atoms ` K )
3 cdlemd.h 
 |-  H = ( LHyp ` K )
4 cdlemd.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> ( K e. HL /\ W e. H ) )
6 simpl2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> F e. T )
7 simpl2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> G e. T )
8 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> ( P e. A /\ -. P .<_ W ) )
9 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> ( F ` P ) = ( G ` P ) )
10 1 2 3 4 cdlemd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( F ` P ) = ( G ` P ) ) -> F = G )
11 5 6 7 8 9 10 syl311anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F ` P ) = ( G ` P ) ) -> F = G )
12 fveq1 
 |-  ( F = G -> ( F ` P ) = ( G ` P ) )
13 12 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) /\ F = G ) -> ( F ` P ) = ( G ` P ) )
14 11 13 impbida 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) = ( G ` P ) <-> F = G ) )