# 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}=\mathrm{LHyp}\left({K}\right)$
cdlemk7.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk7.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk7.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion cdlemk ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {N}\in {T}\right)\wedge {R}\left({F}\right)={R}\left({N}\right)\right)\to \exists {u}\in {E}\phantom{\rule{.4em}{0ex}}{u}\left({F}\right)={N}$

### Proof

Step Hyp Ref Expression
1 cdlemk7.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 cdlemk7.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
3 cdlemk7.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
4 cdlemk7.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
6 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
7 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
8 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
9 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
10 eqid ${⊢}\mathrm{oc}\left({K}\right)\left({W}\right)=\mathrm{oc}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)$
12 eqid ${⊢}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)$
13 eqid ${⊢}\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)$
14 eqid ${⊢}\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)=\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)$
15 5 6 7 8 9 1 2 3 10 11 12 13 14 4 cdlemk56w ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {N}\in {T}\right)\wedge {R}\left({F}\right)={R}\left({N}\right)\right)\to \left(\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\in {E}\wedge \left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\left({F}\right)={N}\right)$
16 fveq1 ${⊢}{u}=\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\to {u}\left({F}\right)=\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\left({F}\right)$
17 16 eqeq1d ${⊢}{u}=\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\to \left({u}\left({F}\right)={N}↔\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\left({F}\right)={N}\right)$
18 17 rspcev ${⊢}\left(\left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\in {E}\wedge \left({f}\in {T}⟼if\left({F}={N},{f},\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({f}\right)\right)\to {z}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)=\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({f}\right)\right)\mathrm{meet}\left({K}\right)\left(\left(\left(\mathrm{oc}\left({K}\right)\left({W}\right)\mathrm{join}\left({K}\right){R}\left({b}\right)\right)\mathrm{meet}\left({K}\right)\left({N}\left(\mathrm{oc}\left({K}\right)\left({W}\right)\right)\mathrm{join}\left({K}\right){R}\left({b}\circ {{F}}^{-1}\right)\right)\right)\mathrm{join}\left({K}\right){R}\left({f}\circ {{b}}^{-1}\right)\right)\right)\right)\right)\right)\left({F}\right)={N}\right)\to \exists {u}\in {E}\phantom{\rule{.4em}{0ex}}{u}\left({F}\right)={N}$
19 15 18 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({F}\in {T}\wedge {N}\in {T}\right)\wedge {R}\left({F}\right)={R}\left({N}\right)\right)\to \exists {u}\in {E}\phantom{\rule{.4em}{0ex}}{u}\left({F}\right)={N}$