# Metamath Proof Explorer

## Theorem trlcnv

Description: The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013)

Ref Expression
Hypotheses trlcnv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
trlcnv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
trlcnv.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
Assertion trlcnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {R}\left({{F}}^{-1}\right)={R}\left({F}\right)$

### Proof

Step Hyp Ref Expression
1 trlcnv.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 trlcnv.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
3 trlcnv.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
4 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
5 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
6 4 5 1 lhpexnle ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \exists {p}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}¬{p}{\le }_{{K}}{W}$
7 6 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to \exists {p}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}¬{p}{\le }_{{K}}{W}$
8 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
9 8 1 2 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
10 9 3adant3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
11 simp3l ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {p}\in \mathrm{Atoms}\left({K}\right)$
12 8 5 atbase ${⊢}{p}\in \mathrm{Atoms}\left({K}\right)\to {p}\in {\mathrm{Base}}_{{K}}$
13 11 12 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {p}\in {\mathrm{Base}}_{{K}}$
14 f1ocnvfv1 ${⊢}\left({F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\wedge {p}\in {\mathrm{Base}}_{{K}}\right)\to {{F}}^{-1}\left({F}\left({p}\right)\right)={p}$
15 10 13 14 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {{F}}^{-1}\left({F}\left({p}\right)\right)={p}$
16 15 oveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {F}\left({p}\right)\mathrm{join}\left({K}\right){{F}}^{-1}\left({F}\left({p}\right)\right)={F}\left({p}\right)\mathrm{join}\left({K}\right){p}$
17 simp1l ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {K}\in \mathrm{HL}$
18 4 5 1 2 ltrnat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {p}\in \mathrm{Atoms}\left({K}\right)\right)\to {F}\left({p}\right)\in \mathrm{Atoms}\left({K}\right)$
19 18 3adant3r ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {F}\left({p}\right)\in \mathrm{Atoms}\left({K}\right)$
20 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
21 20 5 hlatjcom ${⊢}\left({K}\in \mathrm{HL}\wedge {F}\left({p}\right)\in \mathrm{Atoms}\left({K}\right)\wedge {p}\in \mathrm{Atoms}\left({K}\right)\right)\to {F}\left({p}\right)\mathrm{join}\left({K}\right){p}={p}\mathrm{join}\left({K}\right){F}\left({p}\right)$
22 17 19 11 21 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {F}\left({p}\right)\mathrm{join}\left({K}\right){p}={p}\mathrm{join}\left({K}\right){F}\left({p}\right)$
23 16 22 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {F}\left({p}\right)\mathrm{join}\left({K}\right){{F}}^{-1}\left({F}\left({p}\right)\right)={p}\mathrm{join}\left({K}\right){F}\left({p}\right)$
24 23 oveq1d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left({F}\left({p}\right)\mathrm{join}\left({K}\right){{F}}^{-1}\left({F}\left({p}\right)\right)\right)\mathrm{meet}\left({K}\right){W}=\left({p}\mathrm{join}\left({K}\right){F}\left({p}\right)\right)\mathrm{meet}\left({K}\right){W}$
25 simp1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
26 1 2 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {{F}}^{-1}\in {T}$
27 26 3adant3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {{F}}^{-1}\in {T}$
28 4 5 1 2 ltrnel ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to \left({F}\left({p}\right)\in \mathrm{Atoms}\left({K}\right)\wedge ¬{F}\left({p}\right){\le }_{{K}}{W}\right)$
29 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
30 4 20 29 5 1 2 3 trlval2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {{F}}^{-1}\in {T}\wedge \left({F}\left({p}\right)\in \mathrm{Atoms}\left({K}\right)\wedge ¬{F}\left({p}\right){\le }_{{K}}{W}\right)\right)\to {R}\left({{F}}^{-1}\right)=\left({F}\left({p}\right)\mathrm{join}\left({K}\right){{F}}^{-1}\left({F}\left({p}\right)\right)\right)\mathrm{meet}\left({K}\right){W}$
31 25 27 28 30 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({{F}}^{-1}\right)=\left({F}\left({p}\right)\mathrm{join}\left({K}\right){{F}}^{-1}\left({F}\left({p}\right)\right)\right)\mathrm{meet}\left({K}\right){W}$
32 4 20 29 5 1 2 3 trlval2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({F}\right)=\left({p}\mathrm{join}\left({K}\right){F}\left({p}\right)\right)\mathrm{meet}\left({K}\right){W}$
33 24 31 32 3eqtr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({{F}}^{-1}\right)={R}\left({F}\right)$
34 33 3expa ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\wedge \left({p}\in \mathrm{Atoms}\left({K}\right)\wedge ¬{p}{\le }_{{K}}{W}\right)\right)\to {R}\left({{F}}^{-1}\right)={R}\left({F}\right)$
35 7 34 rexlimddv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {R}\left({{F}}^{-1}\right)={R}\left({F}\right)$