Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

ArticleOn n-dimensional Real Spaces and n-dimensional
Complex Spaces I
中村 八束 1,*Yatsuka Nakamura1,*
1 信州大学名誉教授. 長野県長野市青木島
1 Shinshu University, Professor Emeritus. Aokijima, Nagano, Japan* jaceks19731005@gmail.com
ID: MOMENTM1
Proof checked by Mizar Version: 8.1.08 and MML Version: 5.53.1335
Received: November 27, 2020. Accepted: April 30, 2021.

Abstract
A stationary object and a moving object are diﬀerent entities. Light, heat, electromagnetic waves, and the moving stars of the universe have similar characteristics. In
conventional physics, the state of an object is described by a combination of the coordinates q of position and the coordinates p of momentum. In fact, this description method
is suitable for describing the state of many other physical quantities. We develop a basic
theory that expresses the duality of such existence.
静止している物体と，運動している物体とでは異なる存在である．光も熱も電磁波も宇宙の運動する宇宙の星々も同様な特徴を持つ．従来の物理学では，位置の座標 q と運動量の座標 p の座標の組み合わせで物体の状態を記述した．実はこの記述法は，他の多くの物理量の状態記述に適しているのである．そのような存在の二面性を表現する基礎理論を展開する．

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

1/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

Mizar article information
Works in Progress
MOMENTM1 On n-dimensional Real Spaces and n-dimensional Complex Spaces I
by Yatsuka Nakamura
Listing 1. MOMENTM1 - abstract (momentm1.abs):::: On n−dimensional Real Spaces and n−dimensional Complex Spaces I:: 19. Nov. 2020:: Yatsuka Nakamura
environvocabularies TARSKI, NUMBERS, NAT 1, FINSEQ 2, FINSEQ 1, SUBSET 1, SQUARE 1,
VALUED 0, CARD 1, XXREAL 0, XCMPLX 0, FUNCT 1, FUNCT 2, FUNCT 7,XBOOLE 0, RVSUM 1, COMPLEX1, RELAT 1, REAL 1, ARYTM 1, MOMENTM1;
notations TARSKI, XBOOLE 0, VALUED 0, FUNCT 1, FUNCT 2, ORDINAL1, CARD 1,
NUMBERS, XCMPLX 0, XREAL 0, COMPLEX1, FINSEQ 1, FINSEQ 2, DOMAIN 1,RELAT 1, XXREAL 0, SUBSET 1, EUCLID;
constructors COMPLEX1, FINSEQOP, TOPMETR, EUCLID;
registrations RELSET 1, NUMBERS, XREAL 0, FINSEQ 2, RVSUM 1, ORDINAL1,COMPLEX1, XCMPLX 0;
requirements NUMERALS, SUBSET, BOOLE;
deﬁnitions TARSKI;
equalities EUCLID, FINSEQ 1, FINSEQ 2;
expansions TARSKI, XBOOLE 0;
theorems FINSEQ 1, FINSEQ 2, FUNCT 1, FUNCT 2, TARSKI, COMPLEX1, FUNCOP 1,
ORDINAL1, NUMBERS, XBOOLE 1;
begin
reserve a,b,c,d for Real;reserve x,y,x3,y3,X,z,Y,Z,V for set;
theorem :: MOMENTM1:1(REAL) c= COMPLEX;
theorem :: MOMENTM1:2 ::CCD20:<i> in COMPLEX;
theorem :: MOMENTM1:3 ::CCD21:<i>∗<i> = −1r;
theorem :: MOMENTM1:4
not <i> in REAL;
theorem :: MOMENTM1:5 ::CCC21:(REAL) c< COMPLEX;
theorem :: MOMENTM1:6
REAL∗ is FinSequenceSet of REAL;
theorem :: MOMENTM1:7
COMPLEX∗ is FinSequenceSet of COMPLEX;
theorem :: MOMENTM1:8
REAL∗ is FinSequenceSet of COMPLEX;
theorem :: MOMENTM1:9
REAL∗ c= COMPLEX∗;
deﬁnition
let n be Nat;func COMPLEX n −> FinSequenceSet of COMPLEX equals

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

2/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.):: MOMENTM1:def 1
n−tuples on COMPLEX;
end;registration
let n be Nat;cluster COMPLEX n −> non empty;
end;registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;
end;theorem :: MOMENTM1:10
for n being Nat holds
REAL n = n−tuples on REAL;
theorem :: MOMENTM1:11
for n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
registration
let n be Nat;cluster −> n−element for Element of (COMPLEX n);
end;theorem :: MOMENTM1:12
for n being Nat holds
REAL n = n−tuples on REAL;
theorem :: MOMENTM1:13
for n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
theorem :: MOMENTM1:14
for n being Nat holds
REAL n is FinSequenceSet of REAL;
theorem :: MOMENTM1:15
for n being Nat holds
COMPLEX n is FinSequenceSet of COMPLEX;
registration
let n be Nat;cluster COMPLEX n −> non empty;
end;registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;
end;theorem :: MOMENTM1:16 ::CCC22:
for n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
reserve z for Complex;
reserve x,x3,y,z,P,Q,X,Y,Z for set;
theorem :: MOMENTM1:17
for n being Nat holds
n−tuples on REAL = Funcs(Seg n,REAL);
theorem :: MOMENTM1:18
for n being Nat holds
n−tuples on COMPLEX = Funcs(Seg n,COMPLEX);
theorem :: MOMENTM1:19

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

3/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

for x being object,n being Nat holds
x in Funcs(Seg n,REAL) iﬀ ex f being Function st x = f &dom f = Seg n & rng f c= REAL;
theorem :: MOMENTM1:20
for x being object,n being Nat holds
x in Funcs(Seg n,COMPLEX) iﬀ ex f being Function st x = f &dom f = Seg n & rng f c= COMPLEX;
theorem :: MOMENTM1:21
for n being Nat holds
n−tuples on COMPLEX = Funcs(Seg n,COMPLEX);
theorem :: MOMENTM1:22
for n being Nat holds
Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX);
theorem :: MOMENTM1:23
for n being Nat holds (n−tuples on REAL)
c= (n−tuples on COMPLEX);
theorem :: MOMENTM1:24
for n being Nat holds (REAL n) c= (COMPLEX n);
reserve f for real−valued FinSequence;deﬁnition
let n be Nat;func I∗n −> FinSequence equals:: MOMENTM1:def 2n |−> In(1,REAL);
end;
deﬁnition
let n be Nat;func i∗n −> complex−valued FinSequence equals:: MOMENTM1:def 3n |−> In(<i>,COMPLEX);
end;
theorem :: MOMENTM1:25 ::CCC525:
for n being Nat holdsi∗n is Element of COMPLEX n;theorem :: MOMENTM1:26 ::CCC526:
for n being Nat st 1 <= nholds i∗n in COMPLEX n;registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;
end;theorem :: MOMENTM1:27
for n being Nat st 1 <= nholds rng (i∗n) = {<i>} &ex f2 being Function stdom f2 = Seg n & rng f2 c= COMPLEX;
theorem :: MOMENTM1:28
for n being Nat
holds Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX);
theorem :: MOMENTM1:29
for n being Nat st 1 <= nholds i∗ n in Funcs(Seg n,COMPLEX)& not i∗ n in Funcs(Seg n,REAL);
theorem :: MOMENTM1:30

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

4/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

for n being Nat st 1 <= nholds Funcs(Seg n,REAL)c< Funcs(Seg n,COMPLEX);
theorem :: MOMENTM1:31
for n being Nat st n>=1holds (n−tuples on REAL) c< (n−tuples on COMPLEX);
theorem :: MOMENTM1:32
for n being Nat st n>=1
holds (REAL n) c< (COMPLEX n);

Listing 2. MOMENTM1 - vocabulary (momentm1.voc)
OI∗
Oi∗

Listing 3. MOMENTM1 - article (momentm1.miz):::: On n−dimensional Real Spaces and n−dimensional Complex Spaces I:: 19. Nov. 2020:: Yatsuka Nakamura
environvocabularies TARSKI, NUMBERS, NAT 1, FINSEQ 2, FINSEQ 1, SUBSET 1, SQUARE 1,VALUED 0, CARD 1, XXREAL 0, XCMPLX 0, FUNCT 1, FUNCT 2, FUNCT 7,
XBOOLE 0, RVSUM 1, COMPLEX1, RELAT 1, REAL 1, ARYTM 1, MOMENTM1;
notations TARSKI, XBOOLE 0, VALUED 0, FUNCT 1, FUNCT 2, ORDINAL1, CARD 1,NUMBERS, XCMPLX 0, XREAL 0, COMPLEX1, FINSEQ 1, FINSEQ 2, DOMAIN 1,RELAT 1, XXREAL 0, SUBSET 1, EUCLID;constructors COMPLEX1, FINSEQOP, TOPMETR, EUCLID;
registrations RELSET 1, NUMBERS, XREAL 0, FINSEQ 2, RVSUM 1, ORDINAL1,COMPLEX1, XCMPLX 0;
requirements NUMERALS, SUBSET, BOOLE;
deﬁnitions TARSKI;
equalities EUCLID, FINSEQ 1, FINSEQ 2;
expansions TARSKI, XBOOLE 0;
theorems FINSEQ 1, FINSEQ 2, FUNCT 1, FUNCT 2, TARSKI, COMPLEX1, FUNCOP 1,ORDINAL1, NUMBERS, XBOOLE 1;
begin
reserve a,b,c,d for Real;reserve x,y,x3,y3,X,z,Y,Z,V for set;
theorem Th1:(REAL) c= COMPLEX by NUMBERS:11;
theorem ::CCD20:<i> in COMPLEX;
theorem ::CCD21:<i>∗<i> = −1r by COMPLEX1:18;
theorem Th4:
not <i> in REAL by COMPLEX1:7;
theorem ::CCC21:(REAL) c< COMPLEX by Th4,Th1;
theorem
REAL∗ is FinSequenceSet of REAL;

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

5/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

theorem
COMPLEX∗ is FinSequenceSet of COMPLEX;
theorem Th8: REAL∗ is FinSequenceSet of COMPLEX
by FINSEQ 2:91,Th1;
theorem
REAL∗ c= COMPLEX∗ by FINSEQ 2:90,Th8;
deﬁnition
let n be Nat;func COMPLEX n −> FinSequenceSet of COMPLEX equals
n−tuples on COMPLEX;
coherence;
end;
registration
let n be Nat;cluster COMPLEX n −> non empty;
coherence;
end;
registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;coherence;
end;
theoremfor n being Nat holds
REAL n = n−tuples on REAL;
theoremfor n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
registration
let n be Nat;cluster −> n−element for Element of (COMPLEX n);coherence;
end;
theoremfor n being Nat holds
REAL n = n−tuples on REAL;
theoremfor n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
theoremfor n being Nat holds
REAL n is FinSequenceSet of REAL;
theoremfor n being Nat holds
COMPLEX n is FinSequenceSet of COMPLEX;
registration
let n be Nat;cluster COMPLEX n −> non empty;
coherence;
end;
registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;coherence;end;

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

6/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

theorem ::CCC22:
for n being Nat holds
COMPLEX n = n−tuples on COMPLEX;
reserve z for Complex;
reserve x,x3,y,z,P,Q,X,Y,Z for set;
theorem Th17:
for n being Nat holds
n−tuples on REAL = Funcs(Seg n,REAL) by FINSEQ 2:93;
theorem Th18:
for n being Nat holds
n−tuples on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ 2:93;
theorem Th19:
for x being object,n being Nat holds
x in Funcs(Seg n,REAL) iﬀ ex f being Function st x = f &dom f = Seg n & rng f c= REAL by FUNCT 2:def 2;
theorem Th20:
for x being object,n being Nat holds
x in Funcs(Seg n,COMPLEX) iﬀ ex f being Function st x = f &dom f = Seg n & rng f c= COMPLEX by FUNCT 2:def 2;
theorem Th21:
for n being Nat holds
n−tuples on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ 2:93;
theorem Th22:for n being Nat holds
Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)
proof
let n be Nat;thus Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)
proof
let x3 be object;assume x3 in Funcs(Seg n,REAL);thenconsider f be Function such that
A1: x3 = f &dom f = Seg n & rng f c= REAL by Th19;
thus x3 in Funcs(Seg n,COMPLEX) by Th1,Th20,XBOOLE 1:1,A1; ::CCC20,end;
end;
theorem Th23:
for n being Nat holds (n−tuples on REAL)c= (n−tuples on COMPLEX)
proof
let n be Nat;now let x3 being object;assume A1: x3 in (n−tuples on REAL);
A2: Funcs(Seg n,REAL) c= Funcs(Seg n,COMPLEX) by Th22;
x3 in Funcs(Seg n,REAL)by Th17,A1;thenx3 in Funcs(Seg n,COMPLEX)by A2;
hence x3 in (n−tuples on COMPLEX)by Th21;
end;
hence thesis;
end;theoremfor n being Nat holds (REAL n) c= (COMPLEX n) by Th23;
reserve f for real−valued FinSequence;deﬁnition
let n be Nat;func I∗n −> FinSequence equalsn |−> In(1,REAL);

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

7/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

correctness;end;
deﬁnition
let n be Nat;func i∗n −> complex−valued FinSequence equalsn |−> In(<i>,COMPLEX);
correctness;end;
theorem ::CCC525:
for n being Nat holdsi∗n is Element of COMPLEX n;theorem ::CCC526:
for n being Nat st 1 <= nholds i∗n in COMPLEX n;registration
let n be Nat;cluster −> n−element for Element of COMPLEX n;correctness;end;
theorem Th27:
for n being Nat st 1 <= nholds rng (i∗n) = {<i>} &ex f2 being Function st
dom f2 = Seg n & rng f2 c= COMPLEX
proof
let n be Nat;assume A1: 1 <= n;A2: 1 in Seg n by A1;
A3: n is Element of NAT by ORDINAL1:def 12;
for A being set, p being FinSequence ofA holds p in n −tuples on A iﬀ len p = n by FINSEQ 2:133,A3;thenA4: for p being FinSequence of COMPLEX holds( p in n −tuples on COMPLEX iﬀ len p = n );A5: i∗ n in n −tuples on COMPLEX iﬀ len (i∗ n) = n by A4;
A6: len (i∗ n) = n by A5;
A7: Seg len (i∗ n) = dom (i∗ n) by FINSEQ 1:def 3;
A8: len (i∗ n) =n by A6;then
A9: dom (i∗n) = Seg n by A7;
1 in { k where k is Nat : ( 1 <= k & k <= n ) } by A2;then
A10: 1 in Seg n;then
A11: 1 in dom (i∗n) by A9;
A12: (n |−> In(<i>,COMPLEX)).1 = In(<i>,COMPLEX)by A10,FUNCOP 1:7;
reconsider p = (n |−> In(<i>,COMPLEX)) as FinSequence;
A13: Seg len p = dom p by FINSEQ 1:def 3;
p.1 = In(<i>,COMPLEX) by A12; then
A14: (n |−> <i>).1= In(<i>,COMPLEX).= <i> ;A15: (n |−> In(<i>,COMPLEX)).1= <i> by A14;
rng (n |−> In(<i>,COMPLEX))= {<i>}proof
A16: rng(n |−> In(<i>,COMPLEX)) c= {<i>}proof let y3 be object;assume y3 in rng(n |−> In(<i>,COMPLEX));thenconsider x3 being object such that
A17: x3 in dom (n |−> In(<i>,COMPLEX))& (n |−> In(<i>,COMPLEX)).x3 = y3 by FUNCT 1:def 3;
x3 in dom (n |−> In(<i>,COMPLEX)) by A17;thenx3 in Seg n by A13,A8;thenx3 in Seg n ;then
A18: (n |−> In(<i>,COMPLEX)).x3 = In(<i>,COMPLEX)by FUNCOP 1:7;

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

8/10Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)(n |−> <i>).x3= In(<i>,COMPLEX) by A18.= <i> ;then
A19: (n |−> In(<i>,COMPLEX)).x3= <i>;A20: x3 in dom (n |−> In(<i>,COMPLEX))& (n |−> In(<i>,COMPLEX)).x3= y3 by A17;
y3= <i> by A20,A19;
hence y3 in {<i>} by TARSKI:def 1;end;{<i>} c= rng(n |−> In(<i>,COMPLEX))
proof let y3 be object;assume y3 in {<i>};thenA21: y3= <i> by TARSKI:def 1;
A22: 1 in dom (n |−> In(<i>,COMPLEX)) by A11;
1 in dom (n |−> In(<i>,COMPLEX))& (n |−> In(<i>,COMPLEX)).1= y3 by A21,A22,A15;
hence y3 in rng(n |−> In(<i>,COMPLEX)) by FUNCT 1:def 3;
end;hence thesis by A16;
end;
hence rng (i∗n) = {<i>} &ex f2 being Function st
dom f2 = Seg n & rng f2 c= COMPLEX by A9;
end;
theorem Th28:
for n being Nat
holds Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX) by Th22;theorem Th29:
for n being Nat st 1 <= nholds i∗ n in Funcs(Seg n,COMPLEX)& not i∗ n in Funcs(Seg n,REAL)
proof let n be Nat;assume A1: 1 <= n;n−tuples on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ 2:93;thenA2: i∗ n in Funcs(Seg n,COMPLEX);
1 in { k where k is Nat: 1 <= k & k <= n } by A1;thenA3: 1 in Seg n;
A4: not <i> in REAL by Th4;
now assume A5: i∗ n in Funcs(Seg n,REAL);
consider f be Function such that
A6: (i∗ n) = f & dom f = Seg n & rng f c= REAL by A5,FUNCT 2:def 2;
1 in Seg n by A3;thenA7: (i∗ n).1 in rng (i∗ n) by A6,FUNCT 1:def 3;(i∗n).1 in {<i>} by A7,A1,Th27;thenA8: (i∗n).1 = <i> by TARSKI:def 1;<i> in REAL by A8,A7,A6;
hence contradiction by A4;
end;then
not i∗ n in Funcs(Seg n,REAL);
hence thesis by A2;
end;theorem Th30:
for n being Nat st 1 <= nholds Funcs(Seg n,REAL)c< Funcs(Seg n,COMPLEX)
proof let n be Nat;assume A1: 1 <= n;A2: Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)by Th28;
now assume A3: Funcs(Seg n,REAL)= Funcs(Seg n,COMPLEX);i∗ n in Funcs(Seg n,COMPLEX) by Th29,A1;
hence contradiction by A3,Th29,A1;
end;
hence thesis by A2;
end;

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

9/10

Mechanized Mathematics and Its Applications, Works in Progress

On n-dimensional Real Spaces (Nakamura Y.)

theorem Th31:for n being Nat st n>=1
holds (n−tuples on REAL) c< (n−tuples on COMPLEX)
proof let n be Nat;assume A1: n>=1;
A2: Funcs(Seg n,REAL)=(n−tuples on REAL) by Th17;
Funcs(Seg n,COMPLEX)=(n−tuples on COMPLEX) by Th18;
hence thesis by A1,A2,Th30;
end;theoremfor n being Nat st n>=1
holds (REAL n) c< (COMPLEX n) by Th31;

MMA-WiP (2021), vol.3, no.1 - https://mizar-jp.org/journal/MMA-WiP/j2021.3.1 - ISSN 2434-5458 (Online)

10/10