let A be non empty set ; for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric
let L be lower-bounded LATTICE; for O being Ordinal
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric
let O be Ordinal; for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric
let d be BiFunction of A,L; ( d is symmetric implies for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric )
assume A1:
d is symmetric
; for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric
let q be QuadrSeq of d; ConsecutiveDelta (q,O) is symmetric
defpred S1[ Ordinal] means ConsecutiveDelta (q,$1) is symmetric ;
A2:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
assume
ConsecutiveDelta (
q,
O1) is
symmetric
;
S1[ succ O1]
then A3:
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1))) is
symmetric
by Th17;
let x,
y be
Element of
ConsecutiveSet (
A,
(succ O1));
LATTICE5:def 5 (ConsecutiveDelta (q,(succ O1))) . (x,y) = (ConsecutiveDelta (q,(succ O1))) . (y,x)
reconsider x9 =
x,
y9 =
y as
Element of
new_set (ConsecutiveSet (A,O1)) by Th22;
A4:
ConsecutiveDelta (
q,
(succ O1)) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),
(Quadr (q,O1)))
by Th27
.=
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1)))
by Def15
;
hence (ConsecutiveDelta (q,(succ O1))) . (
x,
y) =
(new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (
y9,
x9)
by A3
.=
(ConsecutiveDelta (q,(succ O1))) . (
y,
x)
by A4
;
verum
end;
A5:
for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) holds
S1[O2]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet (A,$1)),
L =
ConsecutiveDelta (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) implies S1[O2] )
assume that A6:
(
O2 <> 0 &
O2 is
limit_ordinal )
and A7:
for
O1 being
Ordinal st
O1 in O2 holds
ConsecutiveDelta (
q,
O1) is
symmetric
;
S1[O2]
set CS =
ConsecutiveSet (
A,
O2);
consider Ls being
Sequence such that A8:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
ConsecutiveDelta (
q,
O2)
= union (rng Ls)
by A6, A8, Th28;
then reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet (A,O2)),
L ;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet (
A,$1);
consider Ts being
Sequence such that A9:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A10:
ConsecutiveSet (
A,
O2)
= union (rng Ts)
by A6, A9, Th23;
f is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet (
A,
O2);
LATTICE5:def 5 f . (x,y) = f . (y,x)
consider x1 being
set such that A11:
x in x1
and A12:
x1 in rng Ts
by A10, TARSKI:def 4;
consider o1 being
object such that A13:
o1 in dom Ts
and A14:
x1 = Ts . o1
by A12, FUNCT_1:def 3;
consider y1 being
set such that A15:
y in y1
and A16:
y1 in rng Ts
by A10, TARSKI:def 4;
consider o2 being
object such that A17:
o2 in dom Ts
and A18:
y1 = Ts . o2
by A16, FUNCT_1:def 3;
reconsider o1 =
o1,
o2 =
o2 as
Ordinal by A13, A17;
A19:
x in ConsecutiveSet (
A,
o1)
by A9, A11, A13, A14;
A20:
Ls . o1 = ConsecutiveDelta (
q,
o1)
by A8, A9, A13;
then reconsider h1 =
Ls . o1 as
BiFunction of
(ConsecutiveSet (A,o1)),
L ;
A21:
h1 is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet (
A,
o1);
LATTICE5:def 5 h1 . (x,y) = h1 . (y,x)
A22:
ConsecutiveDelta (
q,
o1) is
symmetric
by A7, A9, A13;
thus h1 . (
x,
y) =
(ConsecutiveDelta (q,o1)) . (
x,
y)
by A8, A9, A13
.=
(ConsecutiveDelta (q,o1)) . (
y,
x)
by A22
.=
h1 . (
y,
x)
by A8, A9, A13
;
verum
end;
A23:
dom h1 = [:(ConsecutiveSet (A,o1)),(ConsecutiveSet (A,o1)):]
by FUNCT_2:def 1;
A24:
y in ConsecutiveSet (
A,
o2)
by A9, A15, A17, A18;
A25:
Ls . o2 = ConsecutiveDelta (
q,
o2)
by A8, A9, A17;
then reconsider h2 =
Ls . o2 as
BiFunction of
(ConsecutiveSet (A,o2)),
L ;
A26:
h2 is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet (
A,
o2);
LATTICE5:def 5 h2 . (x,y) = h2 . (y,x)
A27:
ConsecutiveDelta (
q,
o2) is
symmetric
by A7, A9, A17;
thus h2 . (
x,
y) =
(ConsecutiveDelta (q,o2)) . (
x,
y)
by A8, A9, A17
.=
(ConsecutiveDelta (q,o2)) . (
y,
x)
by A27
.=
h2 . (
y,
x)
by A8, A9, A17
;
verum
end;
A28:
dom h2 = [:(ConsecutiveSet (A,o2)),(ConsecutiveSet (A,o2)):]
by FUNCT_2:def 1;
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose
o1 c= o2
;
f . (x,y) = f . (y,x)then A29:
ConsecutiveSet (
A,
o1)
c= ConsecutiveSet (
A,
o2)
by Th29;
then A30:
[y,x] in dom h2
by A19, A24, A28, ZFMISC_1:87;
ConsecutiveDelta (
q,
o2)
in rng Ls
by A8, A9, A17, A25, FUNCT_1:def 3;
then A31:
h2 c= f
by A25, ZFMISC_1:74;
reconsider x9 =
x,
y9 =
y as
Element of
ConsecutiveSet (
A,
o2)
by A9, A15, A17, A18, A19, A29;
[x,y] in dom h2
by A19, A24, A28, A29, ZFMISC_1:87;
hence f . (
x,
y) =
h2 . (
x9,
y9)
by A31, GRFUNC_1:2
.=
h2 . (
y9,
x9)
by A26
.=
f . (
y,
x)
by A31, A30, GRFUNC_1:2
;
verum end; suppose
o2 c= o1
;
f . (x,y) = f . (y,x)then A32:
ConsecutiveSet (
A,
o2)
c= ConsecutiveSet (
A,
o1)
by Th29;
then A33:
[y,x] in dom h1
by A19, A24, A23, ZFMISC_1:87;
ConsecutiveDelta (
q,
o1)
in rng Ls
by A8, A9, A13, A20, FUNCT_1:def 3;
then A34:
h1 c= f
by A20, ZFMISC_1:74;
reconsider x9 =
x,
y9 =
y as
Element of
ConsecutiveSet (
A,
o1)
by A9, A11, A13, A14, A24, A32;
[x,y] in dom h1
by A19, A24, A23, A32, ZFMISC_1:87;
hence f . (
x,
y) =
h1 . (
x9,
y9)
by A34, GRFUNC_1:2
.=
h1 . (
y9,
x9)
by A21
.=
f . (
y,
x)
by A34, A33, GRFUNC_1:2
;
verum end;
end;
hence
S1[
O2]
by A6, A8, Th28;
verum
end;
A35:
S1[ 0 ]
proof
let x,
y be
Element of
ConsecutiveSet (
A,
0);
LATTICE5:def 5 (ConsecutiveDelta (q,0)) . (x,y) = (ConsecutiveDelta (q,0)) . (y,x)
reconsider x9 =
x,
y9 =
y as
Element of
A by Th21;
thus (ConsecutiveDelta (q,0)) . (
x,
y) =
d . (
x9,
y9)
by Th26
.=
d . (
y9,
x9)
by A1
.=
(ConsecutiveDelta (q,0)) . (
y,
x)
by Th26
;
verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A35, A2, A5);
hence
ConsecutiveDelta (q,O) is symmetric
; verum