# Metamath Proof Explorer

## Theorem ltrneq2

Description: The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014)

Ref Expression
Hypotheses ltrneq2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
ltrneq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
ltrneq2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
Assertion ltrneq2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)↔{F}={G}\right)$

### Proof

Step Hyp Ref Expression
1 ltrneq2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2 ltrneq2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 ltrneq2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 simpl1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
5 simpl3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {G}\in {T}$
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 6 2 3 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
8 4 5 7 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
9 simpl2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}\in {T}$
10 simpr3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {q}\in {A}$
11 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
12 11 1 2 3 ltrncnvat ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {q}\in {A}\right)\to {{F}}^{-1}\left({q}\right)\in {A}$
13 4 9 10 12 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{F}}^{-1}\left({q}\right)\in {A}$
14 6 1 atbase ${⊢}{{F}}^{-1}\left({q}\right)\in {A}\to {{F}}^{-1}\left({q}\right)\in {\mathrm{Base}}_{{K}}$
15 13 14 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{F}}^{-1}\left({q}\right)\in {\mathrm{Base}}_{{K}}$
16 f1ocnvfv1 ${⊢}\left({G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\wedge {{F}}^{-1}\left({q}\right)\in {\mathrm{Base}}_{{K}}\right)\to {{G}}^{-1}\left({G}\left({{F}}^{-1}\left({q}\right)\right)\right)={{F}}^{-1}\left({q}\right)$
17 8 15 16 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{G}}^{-1}\left({G}\left({{F}}^{-1}\left({q}\right)\right)\right)={{F}}^{-1}\left({q}\right)$
18 simpr2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)$
19 fveq2 ${⊢}{p}={{F}}^{-1}\left({q}\right)\to {F}\left({p}\right)={F}\left({{F}}^{-1}\left({q}\right)\right)$
20 fveq2 ${⊢}{p}={{F}}^{-1}\left({q}\right)\to {G}\left({p}\right)={G}\left({{F}}^{-1}\left({q}\right)\right)$
21 19 20 eqeq12d ${⊢}{p}={{F}}^{-1}\left({q}\right)\to \left({F}\left({p}\right)={G}\left({p}\right)↔{F}\left({{F}}^{-1}\left({q}\right)\right)={G}\left({{F}}^{-1}\left({q}\right)\right)\right)$
22 21 rspcv ${⊢}{{F}}^{-1}\left({q}\right)\in {A}\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to {F}\left({{F}}^{-1}\left({q}\right)\right)={G}\left({{F}}^{-1}\left({q}\right)\right)\right)$
23 13 18 22 sylc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}\left({{F}}^{-1}\left({q}\right)\right)={G}\left({{F}}^{-1}\left({q}\right)\right)$
24 6 2 3 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}}$
25 4 9 24 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
26 6 1 atbase ${⊢}{q}\in {A}\to {q}\in {\mathrm{Base}}_{{K}}$
27 10 26 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {q}\in {\mathrm{Base}}_{{K}}$
28 f1ocnvfv2 ${⊢}\left({F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\wedge {q}\in {\mathrm{Base}}_{{K}}\right)\to {F}\left({{F}}^{-1}\left({q}\right)\right)={q}$
29 25 27 28 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}\left({{F}}^{-1}\left({q}\right)\right)={q}$
30 23 29 eqtr3d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {G}\left({{F}}^{-1}\left({q}\right)\right)={q}$
31 30 fveq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{G}}^{-1}\left({G}\left({{F}}^{-1}\left({q}\right)\right)\right)={{G}}^{-1}\left({q}\right)$
32 17 31 eqtr3d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{F}}^{-1}\left({q}\right)={{G}}^{-1}\left({q}\right)$
33 32 breq1d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({{F}}^{-1}\left({q}\right){\le }_{{K}}{x}↔{{G}}^{-1}\left({q}\right){\le }_{{K}}{x}\right)$
34 simpr1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {x}\in {\mathrm{Base}}_{{K}}$
35 f1ocnvfv1 ${⊢}\left({F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {{F}}^{-1}\left({F}\left({x}\right)\right)={x}$
36 25 34 35 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{F}}^{-1}\left({F}\left({x}\right)\right)={x}$
37 36 breq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({{F}}^{-1}\left({q}\right){\le }_{{K}}{{F}}^{-1}\left({F}\left({x}\right)\right)↔{{F}}^{-1}\left({q}\right){\le }_{{K}}{x}\right)$
38 f1ocnvfv1 ${⊢}\left({G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {{G}}^{-1}\left({G}\left({x}\right)\right)={x}$
39 8 34 38 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {{G}}^{-1}\left({G}\left({x}\right)\right)={x}$
40 39 breq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({{G}}^{-1}\left({q}\right){\le }_{{K}}{{G}}^{-1}\left({G}\left({x}\right)\right)↔{{G}}^{-1}\left({q}\right){\le }_{{K}}{x}\right)$
41 33 37 40 3bitr4d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({{F}}^{-1}\left({q}\right){\le }_{{K}}{{F}}^{-1}\left({F}\left({x}\right)\right)↔{{G}}^{-1}\left({q}\right){\le }_{{K}}{{G}}^{-1}\left({G}\left({x}\right)\right)\right)$
42 simpl1l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {K}\in \mathrm{HL}$
43 eqid ${⊢}\mathrm{LAut}\left({K}\right)=\mathrm{LAut}\left({K}\right)$
44 2 43 3 ltrnlaut ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\right)\to {F}\in \mathrm{LAut}\left({K}\right)$
45 4 9 44 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}\in \mathrm{LAut}\left({K}\right)$
46 6 2 3 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {F}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
47 4 9 34 46 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {F}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
48 6 11 43 lautcnvle ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {F}\in \mathrm{LAut}\left({K}\right)\right)\wedge \left({q}\in {\mathrm{Base}}_{{K}}\wedge {F}\left({x}\right)\in {\mathrm{Base}}_{{K}}\right)\right)\to \left({q}{\le }_{{K}}{F}\left({x}\right)↔{{F}}^{-1}\left({q}\right){\le }_{{K}}{{F}}^{-1}\left({F}\left({x}\right)\right)\right)$
49 42 45 27 47 48 syl22anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({q}{\le }_{{K}}{F}\left({x}\right)↔{{F}}^{-1}\left({q}\right){\le }_{{K}}{{F}}^{-1}\left({F}\left({x}\right)\right)\right)$
50 2 43 3 ltrnlaut ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {G}\in \mathrm{LAut}\left({K}\right)$
51 4 5 50 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {G}\in \mathrm{LAut}\left({K}\right)$
52 6 2 3 ltrncl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {G}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
53 4 5 34 52 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to {G}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
54 6 11 43 lautcnvle ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {G}\in \mathrm{LAut}\left({K}\right)\right)\wedge \left({q}\in {\mathrm{Base}}_{{K}}\wedge {G}\left({x}\right)\in {\mathrm{Base}}_{{K}}\right)\right)\to \left({q}{\le }_{{K}}{G}\left({x}\right)↔{{G}}^{-1}\left({q}\right){\le }_{{K}}{{G}}^{-1}\left({G}\left({x}\right)\right)\right)$
55 42 51 27 53 54 syl22anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({q}{\le }_{{K}}{G}\left({x}\right)↔{{G}}^{-1}\left({q}\right){\le }_{{K}}{{G}}^{-1}\left({G}\left({x}\right)\right)\right)$
56 41 49 55 3bitr4d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge \left({x}\in {\mathrm{Base}}_{{K}}\wedge \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\wedge {q}\in {A}\right)\right)\to \left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)$
57 56 3exp2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left({x}\in {\mathrm{Base}}_{{K}}\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to \left({q}\in {A}\to \left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)\right)\right)\right)$
58 57 imp ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to \left({q}\in {A}\to \left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)\right)\right)$
59 58 ralrimdv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to \forall {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)\right)$
60 simpl1l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {K}\in \mathrm{HL}$
61 simpl1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
62 simpl2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {F}\in {T}$
63 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {x}\in {\mathrm{Base}}_{{K}}$
64 61 62 63 46 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {F}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
65 simpl3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {G}\in {T}$
66 61 65 63 52 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to {G}\left({x}\right)\in {\mathrm{Base}}_{{K}}$
67 6 11 1 hlateq ${⊢}\left({K}\in \mathrm{HL}\wedge {F}\left({x}\right)\in {\mathrm{Base}}_{{K}}\wedge {G}\left({x}\right)\in {\mathrm{Base}}_{{K}}\right)\to \left(\forall {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)↔{F}\left({x}\right)={G}\left({x}\right)\right)$
68 60 64 66 67 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left(\forall {q}\in {A}\phantom{\rule{.4em}{0ex}}\left({q}{\le }_{{K}}{F}\left({x}\right)↔{q}{\le }_{{K}}{G}\left({x}\right)\right)↔{F}\left({x}\right)={G}\left({x}\right)\right)$
69 59 68 sylibd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\wedge {x}\in {\mathrm{Base}}_{{K}}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to {F}\left({x}\right)={G}\left({x}\right)\right)$
70 69 ralrimdva ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to \forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
71 24 3adant3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to {F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
72 f1ofn ${⊢}{F}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\to {F}Fn{\mathrm{Base}}_{{K}}$
73 71 72 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to {F}Fn{\mathrm{Base}}_{{K}}$
74 7 3adant2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to {G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}$
75 f1ofn ${⊢}{G}:{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{K}}\to {G}Fn{\mathrm{Base}}_{{K}}$
76 74 75 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to {G}Fn{\mathrm{Base}}_{{K}}$
77 eqfnfv ${⊢}\left({F}Fn{\mathrm{Base}}_{{K}}\wedge {G}Fn{\mathrm{Base}}_{{K}}\right)\to \left({F}={G}↔\forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
78 73 76 77 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left({F}={G}↔\forall {x}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
79 70 78 sylibrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)\to {F}={G}\right)$
80 fveq1 ${⊢}{F}={G}\to {F}\left({p}\right)={G}\left({p}\right)$
81 80 ralrimivw ${⊢}{F}={G}\to \forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)$
82 79 81 impbid1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {F}\in {T}\wedge {G}\in {T}\right)\to \left(\forall {p}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({p}\right)={G}\left({p}\right)↔{F}={G}\right)$