let a, b be Ordinal; for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))
let n be Nat; ( ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) implies a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b))) )
set c = n *^ (exp (omega,b));
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF (n *^ (exp (omega,b))));
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF (n *^ (exp (omega,b))));
assume A1:
( a <> 0 implies b c= omega -exponent (last (CantorNF a)) )
; a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))
per cases
( a = 0 or not 0 in n or ( a <> 0 & 0 in n ) )
;
suppose A4:
(
a <> 0 &
0 in n )
;
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))then consider A0 being
Cantor-normal-form Ordinal-Sequence,
a0 being
Cantor-component Ordinal such that A5:
CantorNF a = A0 ^ <%a0%>
by Th29;
A6:
last (CantorNF a) = a0
by A5, AFINSQ_1:92;
consider c being
Ordinal,
m being
Nat such that A7:
(
0 in Segm m &
a0 = m *^ (exp (omega,c)) )
by ORDINAL5:def 9;
(
0 in m &
m in omega )
by A7, ORDINAL1:def 12;
then A8:
omega -exponent a0 = c
by A7, ORDINAL5:58;
n in omega
by ORDINAL1:def 12;
then A9:
omega -exponent (n *^ (exp (omega,b))) = b
by A4, ORDINAL5:58;
then A10:
a0 (+) (n *^ (exp (omega,b))) = a0 +^ (n *^ (exp (omega,b)))
by A1, A4, A6, A7, A8, Th83;
A11:
a (+) (n *^ (exp (omega,b))) =
(Sum^ (CantorNF a)) (+) (n *^ (exp (omega,b)))
.=
((Sum^ A0) +^ (Sum^ <%a0%>)) (+) (n *^ (exp (omega,b)))
by A5, Th24
.=
((Sum^ A0) (+) (Sum^ <%a0%>)) (+) (n *^ (exp (omega,b)))
by A5, Th84
.=
(Sum^ A0) (+) ((Sum^ <%a0%>) (+) (n *^ (exp (omega,b))))
by Th81
.=
(Sum^ A0) (+) (a0 +^ (n *^ (exp (omega,b))))
by A10, ORDINAL5:53
;
set A =
CantorNF a;
per cases
( b = c or b <> c )
;
suppose A12:
b = c
;
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))set B =
A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>;
A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%> is
Cantor-normal-form
proof
A13:
a0 +^ (n *^ (exp (omega,b))) =
(m +^ n) *^ (exp (omega,c))
by A7, A12, ORDINAL3:46
.=
(m + n) *^ (exp (omega,c))
by CARD_2:36
;
A14:
0 < m
by A7, NAT_1:44;
now for d, e being Ordinal st d in e & e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) holds
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d)let d,
e be
Ordinal;
( d in e & e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) implies omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b2) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b1) )assume A20:
(
d in e &
e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) )
;
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b2) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b1)per cases then
( e in dom A0 or ex k being Nat st
( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & e = (len A0) + k ) )
by AFINSQ_1:20;
suppose A21:
e in dom A0
;
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b2) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b1)then A22:
(
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e = A0 . e &
A0 . e = (CantorNF a) . e )
by A5, ORDINAL4:def 1;
e in (dom A0) +^ (dom <%a0%>)
by A21, ORDINAL3:24, TARSKI:def 3;
then
e in dom (CantorNF a)
by A5, ORDINAL4:def 1;
then A23:
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((CantorNF a) . d)
by A20, A22, ORDINAL5:def 11;
d in dom A0
by A20, A21, ORDINAL1:10;
then
(
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = A0 . d &
A0 . d = (CantorNF a) . d )
by A5, ORDINAL4:def 1;
hence
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d)
by A23;
verum end; suppose
ex
k being
Nat st
(
k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> &
e = (len A0) + k )
;
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b2) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b1)then consider k being
Nat such that A24:
(
k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> &
e = (len A0) + k )
;
A25:
k in Segm 1
by A24, AFINSQ_1:33;
then A26:
k = 0
by NAT_1:44, NAT_1:14;
A27:
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e =
<%(a0 +^ (n *^ (exp (omega,b))))%> . k
by A24, AFINSQ_1:def 3
.=
(m + n) *^ (exp (omega,c))
by A13, A26
;
0 c< m + n
by A14, XBOOLE_1:2, XBOOLE_0:def 8;
then
(
0 in m + n &
m + n in omega )
by ORDINAL1:11, ORDINAL1:def 12;
then A28:
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) = c
by A27, ORDINAL5:58;
A29:
(
(CantorNF a) . d = A0 . d &
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = A0 . d )
by A5, A20, A24, A26, ORDINAL4:def 1;
k in dom <%a0%>
by A25, AFINSQ_1:33;
then A30:
e in dom (CantorNF a)
by A5, A24, AFINSQ_1:23;
omega -exponent ((CantorNF a) . e) = omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e)
by A5, A8, A24, A26, A28, AFINSQ_1:36;
hence
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d)
by A20, A29, A30, ORDINAL5:def 11;
verum end; end; end;
hence
A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%> is
Cantor-normal-form
by A15, ORDINAL5:def 11;
verum
end; then (Sum^ A0) (+) (Sum^ <%(a0 +^ (n *^ (exp (omega,b))))%>) =
(Sum^ A0) +^ (Sum^ <%(a0 +^ (n *^ (exp (omega,b))))%>)
by Th84
.=
(Sum^ A0) +^ (a0 +^ (n *^ (exp (omega,b))))
by ORDINAL5:53
.=
((Sum^ A0) +^ a0) +^ (n *^ (exp (omega,b)))
by ORDINAL3:30
.=
(Sum^ (A0 ^ <%a0%>)) +^ (n *^ (exp (omega,b)))
by ORDINAL5:54
.=
a +^ (n *^ (exp (omega,b)))
by A5
;
hence
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))
by A11, ORDINAL5:53;
verum end; suppose A31:
b <> c
;
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))set B =
A0 ^ <%a0,(n *^ (exp (omega,b)))%>;
A0 ^ <%a0,(n *^ (exp (omega,b)))%> is
Cantor-normal-form
proof
now for d, e being Ordinal st d in e & e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) holds
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)let d,
e be
Ordinal;
( d in e & e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) implies omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1) )A39:
b in c
by A1, A4, A6, A8, A31, XBOOLE_0:def 8, ORDINAL1:11;
assume A40:
(
d in e &
e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) )
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)per cases then
( e in dom A0 or ex k2 being Nat st
( k2 in dom <%a0,(n *^ (exp (omega,b)))%> & e = (len A0) + k2 ) )
by AFINSQ_1:20;
suppose A41:
e in dom A0
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)then A42:
(
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e = A0 . e &
A0 . e = (CantorNF a) . e )
by A5, ORDINAL4:def 1;
e in (dom A0) +^ (dom <%a0%>)
by A41, ORDINAL3:24, TARSKI:def 3;
then
e in dom (CantorNF a)
by A5, ORDINAL4:def 1;
then A43:
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((CantorNF a) . d)
by A40, A42, ORDINAL5:def 11;
d in dom A0
by A40, A41, ORDINAL1:10;
then
(
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = A0 . d &
A0 . d = (CantorNF a) . d )
by A5, ORDINAL4:def 1;
hence
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)
by A43;
verum end; suppose
ex
k2 being
Nat st
(
k2 in dom <%a0,(n *^ (exp (omega,b)))%> &
e = (len A0) + k2 )
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)then consider k2 being
Nat such that A44:
(
k2 in dom <%a0,(n *^ (exp (omega,b)))%> &
e = (len A0) + k2 )
;
k2 in Segm 2
by AFINSQ_1:38, A44;
then A45:
k2 < 2
by NAT_1:44;
d in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>)
by A40, ORDINAL1:10;
per cases then
( d in dom A0 or ex k1 being Nat st
( k1 in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k1 ) )
by AFINSQ_1:20;
suppose A46:
d in dom A0
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)then A47:
(
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = A0 . d &
A0 . d = (CantorNF a) . d )
by A5, ORDINAL4:def 1;
0 in Segm 1
by NAT_1:44;
then
0 in dom <%a0%>
by AFINSQ_1:33;
then
(len A0) + 0 in dom (CantorNF a)
by A5, AFINSQ_1:23;
then
omega -exponent ((CantorNF a) . (len A0)) in omega -exponent ((CantorNF a) . d)
by A46, ORDINAL5:def 11;
then A48:
c in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)
by A5, A8, A47, AFINSQ_1:36;
per cases
( k2 = 0 or k2 = 1 )
by A45, NAT_1:23;
suppose A49:
k2 = 0
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e =
<%a0,(n *^ (exp (omega,b)))%> . k2
by A44, AFINSQ_1:def 3
.=
a0
by A49
;
hence
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)
by A8, A48;
verum end; suppose A50:
k2 = 1
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e =
<%a0,(n *^ (exp (omega,b)))%> . k2
by A44, AFINSQ_1:def 3
.=
n *^ (exp (omega,b))
by A50
;
hence
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)
by A9, A39, A48, ORDINAL1:10;
verum end; end; end; suppose
ex
k1 being
Nat st
(
k1 in dom <%a0,(n *^ (exp (omega,b)))%> &
d = (len A0) + k1 )
;
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b2) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b1)then consider k1 being
Nat such that A51:
(
k1 in dom <%a0,(n *^ (exp (omega,b)))%> &
d = (len A0) + k1 )
;
k1 in Segm 2
by AFINSQ_1:38, A51;
then A52:
k1 < 2
by NAT_1:44;
A53:
(
k1 = 0 &
k2 = 1 )
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d =
<%a0,(n *^ (exp (omega,b)))%> . k1
by A51, AFINSQ_1:def 3
.=
a0
by A53
;
then A55:
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) = c
by A8;
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e =
<%a0,(n *^ (exp (omega,b)))%> . k2
by A44, AFINSQ_1:def 3
.=
n *^ (exp (omega,b))
by A53
;
hence
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)
by A9, A39, A55;
verum end; end; end; end; end;
hence
A0 ^ <%a0,(n *^ (exp (omega,b)))%> is
Cantor-normal-form
by A32, ORDINAL5:def 11;
verum
end; then (Sum^ A0) (+) (Sum^ <%a0,(n *^ (exp (omega,b)))%>) =
(Sum^ A0) +^ (Sum^ <%a0,(n *^ (exp (omega,b)))%>)
by Th84
.=
(Sum^ A0) +^ (a0 +^ (n *^ (exp (omega,b))))
by Th25
.=
((Sum^ A0) +^ a0) +^ (n *^ (exp (omega,b)))
by ORDINAL3:30
.=
(Sum^ (A0 ^ <%a0%>)) +^ (n *^ (exp (omega,b)))
by ORDINAL5:54
.=
a +^ (n *^ (exp (omega,b)))
by A5
;
hence
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))
by A11, Th25;
verum end; end; end; end;