# Metamath Proof Explorer

## Theorem cdlemj3

Description: Part of proof of Lemma J of Crawley p. 118. Eliminate g . (Contributed by NM, 20-Jun-2013)

Ref Expression
Hypotheses cdlemj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemj.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemj.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemj.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion cdlemj3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)$

### Proof

Step Hyp Ref Expression
1 cdlemj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 cdlemj.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 cdlemj.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
5 cdlemj.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
6 simpl1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
8 eqid ${⊢}\mathrm{Atoms}\left({K}\right)=\mathrm{Atoms}\left({K}\right)$
9 7 8 2 lhpexle2 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \exists {u}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)$
10 6 9 syl ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to \exists {u}\in \mathrm{Atoms}\left({K}\right)\phantom{\rule{.4em}{0ex}}\left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)$
11 simpl1l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {K}\in \mathrm{HL}$
12 11 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to {K}\in \mathrm{HL}$
13 simpl1r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {W}\in {H}$
14 13 adantr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to {W}\in {H}$
15 simprl ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to {u}\in \mathrm{Atoms}\left({K}\right)$
16 simprr1 ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to {u}{\le }_{{K}}{W}$
17 1 7 8 2 3 4 cdlemfnid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge {u}{\le }_{{K}}{W}\right)\right)\to \exists {g}\in {T}\phantom{\rule{.4em}{0ex}}\left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)$
18 12 14 15 16 17 syl22anc ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to \exists {g}\in {T}\phantom{\rule{.4em}{0ex}}\left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)$
19 simp1l ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to \left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)$
20 simp1r ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {h}\ne {\mathrm{I}↾}_{{B}}$
21 simp3l ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {g}\in {T}$
22 simp3rr ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {g}\ne {\mathrm{I}↾}_{{B}}$
23 simp2r2 ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {u}\ne {R}\left({F}\right)$
24 23 necomd ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {R}\left({F}\right)\ne {u}$
25 simp3rl ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {R}\left({g}\right)={u}$
26 24 25 neeqtrrd ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {R}\left({F}\right)\ne {R}\left({g}\right)$
27 simp2r3 ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {u}\ne {R}\left({h}\right)$
28 25 27 eqnetrd ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {R}\left({g}\right)\ne {R}\left({h}\right)$
29 1 2 3 4 5 cdlemj2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge \left({h}\ne {\mathrm{I}↾}_{{B}}\wedge {g}\in {T}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({R}\left({F}\right)\ne {R}\left({g}\right)\wedge {R}\left({g}\right)\ne {R}\left({h}\right)\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)$
30 19 20 21 22 26 28 29 syl132anc ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\wedge \left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)$
31 30 3expia ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to \left(\left({g}\in {T}\wedge \left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)\right)$
32 31 expd ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to \left({g}\in {T}\to \left(\left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)\right)\right)$
33 32 rexlimdv ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to \left(\exists {g}\in {T}\phantom{\rule{.4em}{0ex}}\left({R}\left({g}\right)={u}\wedge {g}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)\right)$
34 18 33 mpd ${⊢}\left(\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\wedge \left({u}\in \mathrm{Atoms}\left({K}\right)\wedge \left({u}{\le }_{{K}}{W}\wedge {u}\ne {R}\left({F}\right)\wedge {u}\ne {R}\left({h}\right)\right)\right)\right)\to {U}\left({h}\right)={V}\left({h}\right)$
35 10 34 rexlimddv ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({U}\in {E}\wedge {V}\in {E}\wedge {U}\left({F}\right)={V}\left({F}\right)\right)\wedge \left({F}\in {T}\wedge {F}\ne {\mathrm{I}↾}_{{B}}\wedge {h}\in {T}\right)\right)\wedge {h}\ne {\mathrm{I}↾}_{{B}}\right)\to {U}\left({h}\right)={V}\left({h}\right)$