Metamath Proof Explorer

Theorem cdlemk

Description: Lemma K of Crawley p. 118. Final result, lines 11 and 12 on p. 120: given two translations f and k with the same trace, there exists a trace-preserving endomorphism tau whose value at f is k. We use F , N , and u to represent f, k, and tau. (Contributed by NM, 1-Aug-2013)

Ref Expression
Hypotheses cdlemk7.h 
|- H = ( LHyp ` K )
cdlemk7.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemk7.r 
|- R = ( ( trL ` K ) ` W )
cdlemk7.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion cdlemk 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> E. u e. E ( u ` F ) = N )

Proof

Step Hyp Ref Expression
1 cdlemk7.h 
 |-  H = ( LHyp ` K )
2 cdlemk7.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 cdlemk7.r 
 |-  R = ( ( trL ` K ) ` W )
4 cdlemk7.e 
 |-  E = ( ( TEndo ` K ) ` W )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( meet ` K ) = ( meet ` K )
8 eqid 
 |-  ( oc ` K ) = ( oc ` K )
9 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
11 eqid 
 |-  ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) )
12 eqid 
 |-  ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) )
13 eqid 
 |-  ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) )
14 eqid 
 |-  ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) = ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) )
15 5 6 7 8 9 1 2 3 10 11 12 13 14 4 cdlemk56w 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) e. E /\ ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) ` F ) = N ) )
16 fveq1 
 |-  ( u = ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) -> ( u ` F ) = ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) ` F ) )
17 16 eqeq1d 
 |-  ( u = ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) -> ( ( u ` F ) = N <-> ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) ` F ) = N ) )
18 17 rspcev 
 |-  ( ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) e. E /\ ( ( f e. T |-> if ( F = N , f , ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` ( Base ` K ) ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` f ) ) -> ( z ` ( ( oc ` K ) ` W ) ) = ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` f ) ) ( meet ` K ) ( ( ( ( ( oc ` K ) ` W ) ( join ` K ) ( R ` b ) ) ( meet ` K ) ( ( N ` ( ( oc ` K ) ` W ) ) ( join ` K ) ( R ` ( b o. `' F ) ) ) ) ( join ` K ) ( R ` ( f o. `' b ) ) ) ) ) ) ) ) ` F ) = N ) -> E. u e. E ( u ` F ) = N )
19 15 18 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> E. u e. E ( u ` F ) = N )