The first "hilims" example shows unification (and proof construction) with work variables still in the proof.
Note that "hilims" variables are almost all "dummy" variables, but that some of the work variables got resolved into "dummy" variables during unification -- leaving a mixture of dummy variables and work variables.
The second "hilims" example shows the new mmj2 "work variable to dummy variable" conversion algorithm, which replaces any remaining work variables with dummy variables.
As you can determine by comparing the second example with the original "hilims" proof -- step 10 for example – in some cases where "x" is already in the proof step, mmj2 substitutes a different dummy variable, such as "w".
The reason for this is that although a "dummy" should be freely substitutable with another dummy in most cases popping up in mmj2 now, there is the theoretical possibility that substituting "x" into a formula that already contains "x" could result in a "hard" Distinct Variables Requirement error ($d error).
So to be "safe" mmj2 picks an unused dummy variable. This leads to a different issue which is not particularly serious, which is that additional $d statements may be needed on the theorem being proved. Thus, the users will be encouraged to use the "Generate Replacements" or "Generate Differences" RunParm?/Edit Option for Dj Vars editing.
Primarily this is an "issue" when re-processing existing proofs, and is almost a non-issue for new authorship. Still, the new mmj2 algorithm is less parsimonous with dummy variables than, say, Megill would be. Where Megill might require only x, y and z, mmj2 might need x, y, z, u, v and w. (It is very hard to write code that is as smart as Megill!)
If you have any suggestions, comments or complaints, speak up ASAP before I release this code into the wild!
Thanks!
P.S. Something I discovered during testing is that after converting any remaining work variables to dummy variables, the code must redo the Distinct Variable Restriction edits for affected derivation proof steps. Which is not hard, just a tedious gotcha (already coded…)
P.P.S. The proof of "hilims" looks much better with TMFF formatting option 4 - Align Var, Depth 4 -- than the default, Align Column, Depth 3. As a general rule long formulas containing the ".< x , y .>" point/coordinate syntax item look better with option 4 – that is because TMFF gives no weight to a point/coordinate as a single item but treats it the same as any other syntax form involving 2 operands.
$( <MM> <PROOF_ASST> THEOREM=hilims LOC_AFTER=?
* The metric space induced by Hilbert space.
h1::hilims.1 |- D
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
2::df-3an |- ( ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) )
<-> ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) )
3:2:oprabbii |- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
4::fvex |- ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) )
e. V
5::eqid |- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
6:4,5:fnoprab2 |- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
Fn ( H~ X. H~ )
7::fvex |- ( normh ` ( x -h y ) ) e. V
8::eqid |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
9:7,8:fnoprab2 |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
Fn ( H~ X. H~ )
10::eqfnoprval |- ( ( {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
Fn ( H~ X. H~ )
/\ {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
Fn ( H~ X. H~ ) )
-> ( {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
<-> ( ( H~ X. H~ ) = ( H~ X. H~ )
/\ A. &S18
e. H~
A. &S19
e. H~
( &S18
{
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) )
) ) }
&S19 )
= ( &S18
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
&S19 ) ) ) )
11:6,9,10:mp2an |- ( {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
<-> ( ( H~ X. H~ ) = ( H~ X. H~ )
/\ A. &S18
e. H~
A. &S19
e. H~
( &S18
{
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) )
}
&S19 )
= ( &S18
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
&S19 ) ) )
12::eqid |- ( H~ X. H~ ) = ( H~ X. H~ )
13::hvsubvalt |- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( &S18 -h &S19 )
= ( &S18 +h ( -u 1 .h &S19 ) ) )
14:13:eqcomd |- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( &S18 +h ( -u 1 .h &S19 ) )
= ( &S18 -h &S19 ) )
15:14:fveq2d |- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( normh
` ( &S18 +h ( -u 1 .h &S19 ) ) )
= ( normh ` ( &S18 -h &S19 ) ) )
16::fvex |- ( normh
` ( &S18 +h ( -u 1 .h &S19 ) ) )
e. V
17::opreq1 |- ( &S1 = &S18
-> ( &S1 +h ( -u 1 .h &S2 ) )
= ( &S18 +h ( -u 1 .h &S2 ) ) )
18:17:fveq2d |- ( &S1 = &S18
-> ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) )
= ( normh
` ( &S18 +h ( -u 1 .h &S2 ) ) ) )
19::opreq2 |- ( &S2 = &S19
-> ( -u 1 .h &S2 ) = ( -u 1 .h &S19 ) )
20:19:opreq2d |- ( &S2 = &S19
-> ( &S18 +h ( -u 1 .h &S2 ) )
= ( &S18 +h ( -u 1 .h &S19 ) ) )
21:20:fveq2d |- ( &S2 = &S19
-> ( normh
` ( &S18 +h ( -u 1 .h &S2 ) ) )
= ( normh
` ( &S18 +h ( -u 1 .h &S19 ) ) ) )
22::eqid |- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
23:16,18,21,22:oprabval2
|- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( &S18
{
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
&S19 )
= ( normh
` ( &S18 +h ( -u 1 .h &S19 ) ) ) )
24::eqid |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
25:24:hilmsdval |- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( &S18
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
&S19 )
= ( normh ` ( &S18 -h &S19 ) ) )
26:15,23,25:3eqtr4d
|- ( ( &S18 e. H~ /\ &S19 e. H~ )
-> ( &S18
{
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
&S19 )
= ( &S18
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
&S19 ) )
27:26:rgen2 |- A. &S18
e. H~
A. &S19
e. H~
( &S18
{
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
&S19 )
= ( &S18
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
&S19 )
28:11,12,27:mpbir2an
|- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( ( &S1 e. H~ /\ &S2 e. H~ )
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
29:3,28:eqtr |- {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
30:29:opeq2i |- <. H~
, {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >.
= <. H~
, {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) } >.
31::hilncv |- <. <. +h , .h >. , normh >. e. NrmCVec
32::opex |- <. +h , .h >. e. V
33:32:op1st |- ( 1st ` <. <. +h , .h >. , normh >. )
= <. +h , .h >.
34:33:eqcomi |- <. +h , .h >.
= ( 1st ` <. <. +h , .h >. , normh >. )
35::hilabl |- +h e. Abel
36:35:elisseti |- +h e. V
37:36:op1st |- ( 1st ` <. +h , .h >. ) = +h
38:37:eqcomi |- +h = ( 1st ` <. +h , .h >. )
39::hilabl |- +h e. Abel
40:39:elisseti |- +h e. V
41::hvmulex |- .h e. V
42:40,41:op2nd |- ( 2nd ` <. +h , .h >. ) = .h
43:42:eqcomi |- .h = ( 2nd ` <. +h , .h >. )
44::opex |- <. +h , .h >. e. V
45::df-hnorm |- normh
= {
<. &S3
, &S4
>.
| ( &S3 e. H~
/\ &S4 = ( sqr ` ( &S3 .ih &S3 ) ) ) }
46::ax-hilex |- H~ e. V
47:46:funopabex2 |- {
<. &S3
, &S4
>.
| ( &S3 e. H~
/\ &S4 = ( sqr ` ( &S3 .ih &S3 ) ) ) }
e. V
48:45,47:eqeltr |- normh e. V
49:44,48:op2nd |- ( 2nd ` <. <. +h , .h >. , normh >. )
= normh
50:49:eqcomi |- normh
= ( 2nd ` <. <. +h , .h >. , normh >. )
51::hilabl |- +h e. Abel
52::ablgrp |- ( +h e. Abel -> +h e. Grp )
53:51,52:ax-mp |- +h e. Grp
54::ax-hfvadd |- +h : ( H~ X. H~ ) --> H~
55:53,54:grprn |- H~ = ran +h
56:34,38,43,50,55:imsval
|- ( <. <. +h , .h >. , normh >. e. NrmCVec
-> ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~
, {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >. )
57:31,56:ax-mp |- ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~
, {
<.
<. &S1
, &S2
>.
, &S5
>.
| ( &S1 e. H~
/\ &S2 e. H~
/\ &S5
= ( normh
` ( &S1 +h ( -u 1 .h &S2 ) ) ) ) } >.
58:1:opeq2i |- <. H~ , D >.
= <. H~
, {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) } >.
qed:30,57,58:3eqtr4
|- ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~ , D >.
$= chil &S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2
cv csm co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 cop chil vx cv
chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv
wceq wa vx vy vz copab2 cop cva csm cop cno cop cims cfv chil cD cop
&S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm
co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 vx cv chil wcel vy cv
chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz
copab2 chil &S1 cv chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2
cv csm co cva co cno cfv wceq w3a &S1 &S2 &S5 copab2 &S1 cv chil
wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
cno cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil wcel
wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 &S1 cv
chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
cno cfv wceq w3a &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1
cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 &S1 cv
chil wcel &S2 cv chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
cno cfv wceq df-3an oprabbii &S1 cv chil wcel &S2 cv chil wcel wa
&S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1
&S2 &S5 copab2 vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv
cmv co cno cfv wceq wa vx vy vz copab2 wceq chil chil cxp chil chil
cxp wceq &S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv
&S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5
copab2 co &S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx
cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq &S19 chil
wral &S18 chil wral &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1
cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2
chil chil cxp wfn vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy
cv cmv co cno cfv wceq wa vx vy vz copab2 chil chil cxp wfn &S1 cv
chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
co cno cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil
wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq
chil chil cxp chil chil cxp wceq &S18 cv &S19 cv &S1 cv chil wcel
&S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co
cno cfv wceq wa &S1 &S2 &S5 copab2 co &S18 cv &S19 cv vx cv chil
wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx
vy vz copab2 co wceq &S19 chil wral &S18 chil wral wa wb &S1 &S2
&S5 chil chil &S1 cv c1 cneg &S2 cv csm co cva co cno cfv &S1 cv
chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
co cno cfv wceq wa &S1 &S2 &S5 copab2 &S1 cv c1 cneg &S2 cv csm
co cva co cno fvex &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1
cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2
eqid fnoprab2 vx vy vz chil chil vx cv vy cv cmv co cno cfv vx cv
chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa
vx vy vz copab2 vx cv vy cv cmv co cno fvex vx cv chil wcel vy cv
chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz
copab2 eqid fnoprab2 &S18 &S19 chil chil chil chil &S1 cv chil wcel &S2
cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno
cfv wceq wa &S1 &S2 &S5 copab2 vx cv chil wcel vy cv chil wcel wa vz
cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqfnoprval
mp2an chil chil cxp eqid &S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil
wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa
&S1 &S2 &S5 copab2 co &S18 cv &S19 cv vx cv chil wcel vy cv chil
wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co
wceq &S18 &S19 chil &S18 cv chil wcel &S19 cv chil wcel wa &S18 cv c1
cneg &S19 cv csm co cva co cno cfv &S18 cv &S19 cv cmv co cno cfv
&S18 cv &S19 cv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1
cv c1 cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2
co &S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv
vy cv cmv co cno cfv wceq wa vx vy vz copab2 co &S18 cv chil wcel
&S19 cv chil wcel wa &S18 cv c1 cneg &S19 cv csm co cva co &S18 cv
&S19 cv cmv co cno &S18 cv chil wcel &S19 cv chil wcel wa &S18 cv
&S19 cv cmv co &S18 cv c1 cneg &S19 cv csm co cva co &S18 cv &S19 cv
hvsubvalt eqcomd fveq2d &S1 &S2 &S5 &S18 cv &S19 cv chil chil &S1 cv c1
cneg &S2 cv csm co cva co cno cfv &S18 cv c1 cneg &S19 cv csm co cva
co cno cfv &S1 cv chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1
cneg &S2 cv csm co cva co cno cfv wceq wa &S1 &S2 &S5 copab2 &S18 cv
c1 cneg &S2 cv csm co cva co cno cfv &S18 cv c1 cneg &S19 cv csm co
cva co cno fvex &S1 cv &S18 cv wceq &S1 cv c1 cneg &S2 cv csm co
cva co &S18 cv c1 cneg &S2 cv csm co cva co cno &S1 cv &S18 cv c1
cneg &S2 cv csm co cva opreq1 fveq2d &S2 cv &S19 cv wceq &S18 cv c1
cneg &S2 cv csm co cva co &S18 cv c1 cneg &S19 cv csm co cva co cno
&S2 cv &S19 cv wceq c1 cneg &S2 cv csm co c1 cneg &S19 cv csm co
&S18 cv cva &S2 cv &S19 cv c1 cneg csm opreq2 opreq2d fveq2d &S1 cv
chil wcel &S2 cv chil wcel wa &S5 cv &S1 cv c1 cneg &S2 cv csm co cva
co cno cfv wceq wa &S1 &S2 &S5 copab2 eqid oprabval2 vx vy vz
&S18 cv &S19 cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv
cmv co cno cfv wceq wa vx vy vz copab2 vx cv chil wcel vy cv chil
wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqid
hilmsdval 3eqtr4d rgen2 mpbir2an eqtr opeq2i cva csm cop cno cop
cncv wcel cva csm cop cno cop cims cfv chil &S1 cv chil wcel &S2 cv
chil wcel &S5 cv &S1 cv c1 cneg &S2 cv csm co cva co cno cfv wceq w3a
&S1 &S2 &S5 copab2 cop wceq hilncv &S1 &S2 &S5 csm cva csm cop
cno cop cva cno cva csm cop chil cva csm cop cno cop c1st cfv cva
csm cop cva csm cop cno cva csm opex op1st eqcomi cva csm cop c1st
cfv cva cva csm cva cabl hilabl elisseti op1st eqcomi cva csm cop
c2nd cfv csm cva csm cva cabl hilabl elisseti hvmulex op2nd eqcomi
cva csm cop cno cop c2nd cfv cno cva csm cop cno cva csm opex cno
&S3 cv chil wcel &S4 cv &S3 cv &S3 cv csp co csqr cfv wceq wa &S3
&S4 copab cvv &S3 &S4 df-hnorm &S3 &S4 chil &S3 cv &S3 cv csp co
csqr cfv ax-hilex funopabex2 eqeltr op2nd eqcomi cva chil cva cabl
wcel cva cgr wcel hilabl cva ablgrp ax-mp ax-hfvadd grprn imsval
ax-mp cD vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co
cno cfv wceq wa vx vy vz copab2 chil hilims.1 opeq2i 3eqtr4 $.
$)
$( <MM> <PROOF_ASST> THEOREM=hilims LOC_AFTER=?
* The metric space induced by Hilbert space.
$d x y z u v w f g
h1::hilims.1 |- D
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
2::df-3an |- ( ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) )
<-> ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) )
3:2:oprabbii |- {
<.
<. w
, v
>.
, u
>.
| ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
4::fvex |- ( normh
` ( w +h ( -u 1 .h v ) ) )
e. V
5::eqid |- {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
6:4,5:fnoprab2 |- {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
Fn ( H~ X. H~ )
7::fvex |- ( normh ` ( x -h y ) ) e. V
8::eqid |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
9:7,8:fnoprab2 |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
Fn ( H~ X. H~ )
10::eqfnoprval |- ( ( {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
Fn ( H~ X. H~ )
/\ {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
Fn ( H~ X. H~ ) )
-> ( {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
<-> ( ( H~ X. H~ ) = ( H~ X. H~ )
/\ A. f
e. H~
A. g
e. H~
( f
{
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) )
}
g )
= ( f
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
g ) ) ) )
11:6,9,10:mp2an |- ( {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
<-> ( ( H~ X. H~ ) = ( H~ X. H~ )
/\ A. f
e. H~
A. g
e. H~
( f
{
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
g )
= ( f
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
g ) ) )
12::eqid |- ( H~ X. H~ ) = ( H~ X. H~ )
13::hvsubvalt |- ( ( f e. H~ /\ g e. H~ )
-> ( f -h g )
= ( f +h ( -u 1 .h g ) ) )
14:13:eqcomd |- ( ( f e. H~ /\ g e. H~ )
-> ( f +h ( -u 1 .h g ) )
= ( f -h g ) )
15:14:fveq2d |- ( ( f e. H~ /\ g e. H~ )
-> ( normh
` ( f +h ( -u 1 .h g ) ) )
= ( normh ` ( f -h g ) ) )
16::fvex |- ( normh
` ( f +h ( -u 1 .h g ) ) )
e. V
17::opreq1 |- ( w = f
-> ( w +h ( -u 1 .h v ) )
= ( f +h ( -u 1 .h v ) ) )
18:17:fveq2d |- ( w = f
-> ( normh
` ( w +h ( -u 1 .h v ) ) )
= ( normh
` ( f +h ( -u 1 .h v ) ) ) )
19::opreq2 |- ( v = g
-> ( -u 1 .h v ) = ( -u 1 .h g ) )
20:19:opreq2d |- ( v = g
-> ( f +h ( -u 1 .h v ) )
= ( f +h ( -u 1 .h g ) ) )
21:20:fveq2d |- ( v = g
-> ( normh
` ( f +h ( -u 1 .h v ) ) )
= ( normh
` ( f +h ( -u 1 .h g ) ) ) )
22::eqid |- {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
23:16,18,21,22:oprabval2
|- ( ( f e. H~ /\ g e. H~ )
-> ( f
{
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
g )
= ( normh
` ( f +h ( -u 1 .h g ) ) ) )
24::eqid |- {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
25:24:hilmsdval |- ( ( f e. H~ /\ g e. H~ )
-> ( f
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
g )
= ( normh ` ( f -h g ) ) )
26:15,23,25:3eqtr4d
|- ( ( f e. H~ /\ g e. H~ )
-> ( f
{
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
g )
= ( f
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
g ) )
27:26:rgen2 |- A. f
e. H~
A. g
e. H~
( f
{
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
g )
= ( f
{
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
g )
28:11,12,27:mpbir2an
|- {
<.
<. w
, v
>.
, u
>.
| ( ( w e. H~ /\ v e. H~ )
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
29:3,28:eqtr |- {
<.
<. w
, v
>.
, u
>.
| ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) }
= {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) }
30:29:opeq2i |- <. H~
, {
<.
<. w
, v
>.
, u
>.
| ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) } >.
= <. H~
, {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) } >.
31::hilncv |- <. <. +h , .h >. , normh >. e. NrmCVec
32::opex |- <. +h , .h >. e. V
33:32:op1st |- ( 1st ` <. <. +h , .h >. , normh >. )
= <. +h , .h >.
34:33:eqcomi |- <. +h , .h >.
= ( 1st ` <. <. +h , .h >. , normh >. )
35::hilabl |- +h e. Abel
36:35:elisseti |- +h e. V
37:36:op1st |- ( 1st ` <. +h , .h >. ) = +h
38:37:eqcomi |- +h = ( 1st ` <. +h , .h >. )
39::hilabl |- +h e. Abel
40:39:elisseti |- +h e. V
41::hvmulex |- .h e. V
42:40,41:op2nd |- ( 2nd ` <. +h , .h >. ) = .h
43:42:eqcomi |- .h = ( 2nd ` <. +h , .h >. )
44::opex |- <. +h , .h >. e. V
45::df-hnorm |- normh
= {
<. w
, v
>.
| ( w e. H~
/\ v = ( sqr ` ( w .ih w ) ) ) }
46::ax-hilex |- H~ e. V
47:46:funopabex2 |- {
<. w
, v
>.
| ( w e. H~
/\ v = ( sqr ` ( w .ih w ) ) ) }
e. V
48:45,47:eqeltr |- normh e. V
49:44,48:op2nd |- ( 2nd ` <. <. +h , .h >. , normh >. )
= normh
50:49:eqcomi |- normh
= ( 2nd ` <. <. +h , .h >. , normh >. )
51::hilabl |- +h e. Abel
52::ablgrp |- ( +h e. Abel -> +h e. Grp )
53:51,52:ax-mp |- +h e. Grp
54::ax-hfvadd |- +h : ( H~ X. H~ ) --> H~
55:53,54:grprn |- H~ = ran +h
56:34,38,43,50,55:imsval
|- ( <. <. +h , .h >. , normh >. e. NrmCVec
-> ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~
, {
<.
<. w
, v
>.
, u
>.
| ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) } >. )
57:31,56:ax-mp |- ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~
, {
<.
<. w
, v
>.
, u
>.
| ( w e. H~
/\ v e. H~
/\ u
= ( normh
` ( w +h ( -u 1 .h v ) ) ) ) } >.
58:1:opeq2i |- <. H~ , D >.
= <. H~
, {
<.
<. x
, y
>.
, z
>.
| ( ( x e. H~ /\ y e. H~ )
/\ z = ( normh ` ( x -h y ) ) ) } >.
qed:30,57,58:3eqtr4
|- ( IndMet ` <. <. +h , .h >. , normh >. )
= <. H~ , D >.
$= chil vw cv chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv
csm co cva co cno cfv wceq w3a vw vv vu copab2 cop chil vx cv chil
wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx
vy vz copab2 cop cva csm cop cno cop cims cfv chil cD cop vw cv
chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv csm co cva co cno
cfv wceq w3a vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa
vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 chil vw cv
chil wcel vv cv chil wcel vu cv vw cv c1 cneg vv cv csm co cva co
cno cfv wceq w3a vw vv vu copab2 vw cv chil wcel vv cv chil wcel
wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu
copab2 vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv
co cno cfv wceq wa vx vy vz copab2 vw cv chil wcel vv cv chil wcel
vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq w3a vw cv chil
wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co
cno cfv wceq wa vw vv vu vw cv chil wcel vv cv chil wcel vu cv vw cv
c1 cneg vv cv csm co cva co cno cfv wceq df-3an oprabbii vw cv
chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co
cno cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa
vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq chil
chil cxp chil chil cxp wceq vf cv vg cv vw cv chil wcel vv cv chil
wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vg
chil wral vf chil wral vw cv chil wcel vv cv chil wcel wa vu cv vw cv
c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu copab2 chil
chil cxp wfn vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv
co cno cfv wceq wa vx vy vz copab2 chil chil cxp wfn vw cv chil
wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno
cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa vz cv
vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 wceq chil chil
cxp chil chil cxp wceq vf cv vg cv vw cv chil wcel vv cv chil
wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vg
chil wral vf chil wral wa wb vw vv vu chil chil vw cv c1 cneg vv cv
csm co cva co cno cfv vw cv chil wcel vv cv chil wcel wa vu cv vw cv
c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv vu copab2 vw cv
c1 cneg vv cv csm co cva co cno fvex vw cv chil wcel vv cv chil
wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
vu copab2 eqid fnoprab2 vx vy vz chil chil vx cv vy cv cmv co cno
cfv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co
cno cfv wceq wa vx vy vz copab2 vx cv vy cv cmv co cno fvex vx cv
chil wcel vy cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa
vx vy vz copab2 eqid fnoprab2 vf vg chil chil chil chil vw cv
chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co
cno cfv wceq wa vw vv vu copab2 vx cv chil wcel vy cv chil wcel wa
vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqfnoprval
mp2an chil chil cxp eqid vf cv vg cv vw cv chil wcel vv cv chil
wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq wa vw vv
vu copab2 co vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv
vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 co wceq vf vg
chil vf cv chil wcel vg cv chil wcel wa vf cv c1 cneg vg cv csm co
cva co cno cfv vf cv vg cv cmv co cno cfv vf cv vg cv vw cv chil
wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co cva co cno
cfv wceq wa vw vv vu copab2 co vf cv vg cv vx cv chil wcel vy cv
chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2
co vf cv chil wcel vg cv chil wcel wa vf cv c1 cneg vg cv csm co
cva co vf cv vg cv cmv co cno vf cv chil wcel vg cv chil wcel wa vf
cv vg cv cmv co vf cv c1 cneg vg cv csm co cva co vf cv vg cv
hvsubvalt eqcomd fveq2d vw vv vu vf cv vg cv chil chil vw cv c1 cneg vv cv
csm co cva co cno cfv vf cv c1 cneg vg cv csm co cva co cno cfv
vw cv chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm co
cva co cno cfv wceq wa vw vv vu copab2 vf cv c1 cneg vv cv csm co
cva co cno cfv vf cv c1 cneg vg cv csm co cva co cno fvex vw cv
vf cv wceq vw cv c1 cneg vv cv csm co cva co vf cv c1 cneg vv cv
csm co cva co cno vw cv vf cv c1 cneg vv cv csm co cva opreq1 fveq2d
vv cv vg cv wceq vf cv c1 cneg vv cv csm co cva co vf cv c1 cneg
vg cv csm co cva co cno vv cv vg cv wceq c1 cneg vv cv csm co c1
cneg vg cv csm co vf cv cva vv cv vg cv c1 cneg csm opreq2 opreq2d
fveq2d vw cv chil wcel vv cv chil wcel wa vu cv vw cv c1 cneg vv cv csm
co cva co cno cfv wceq wa vw vv vu copab2 eqid oprabval2 vx vy vz
vf cv vg cv vx cv chil wcel vy cv chil wcel wa vz cv vx cv vy cv
cmv co cno cfv wceq wa vx vy vz copab2 vx cv chil wcel vy cv chil
wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz copab2 eqid
hilmsdval 3eqtr4d rgen2 mpbir2an eqtr opeq2i cva csm cop cno cop
cncv wcel cva csm cop cno cop cims cfv chil vw cv chil wcel vv cv
chil wcel vu cv vw cv c1 cneg vv cv csm co cva co cno cfv wceq w3a vw
vv vu copab2 cop wceq hilncv vw vv vu csm cva csm cop cno cop cva
cno cva csm cop chil cva csm cop cno cop c1st cfv cva csm cop cva
csm cop cno cva csm opex op1st eqcomi cva csm cop c1st cfv cva
cva csm cva cabl hilabl elisseti op1st eqcomi cva csm cop c2nd cfv
csm cva csm cva cabl hilabl elisseti hvmulex op2nd eqcomi cva csm
cop cno cop c2nd cfv cno cva csm cop cno cva csm opex cno vw cv chil
wcel vv cv vw cv vw cv csp co csqr cfv wceq wa vw vv copab cvv vw
vv df-hnorm vw vv chil vw cv vw cv csp co csqr cfv ax-hilex
funopabex2 eqeltr op2nd eqcomi cva chil cva cabl wcel cva cgr wcel hilabl
cva ablgrp ax-mp ax-hfvadd grprn imsval ax-mp cD vx cv chil wcel vy
cv chil wcel wa vz cv vx cv vy cv cmv co cno cfv wceq wa vx vy vz
copab2 chil hilims.1 opeq2i 3eqtr4 $.
$)