let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
let A be non-empty MSAlgebra over S; for R being ManySortedRelation of A holds
( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
let R be ManySortedRelation of A; ( R is invariant iff for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 )
hereby ( ( for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2 ) implies R is invariant )
defpred S1[
Function,
set ,
set ]
means for
a,
b being
set st
[a,b] in R . $2 holds
[($1 . a),($1 . b)] in R . $3;
deffunc H1(
SortSymbol of
S)
-> Element of
bool [:( the Sorts of A . $1),( the Sorts of A . $1):] =
id ( the Sorts of A . $1);
assume A1:
R is
invariant
;
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for t being Translation of A,s1,s2 holds S1[t,s1,s2]A2:
for
s1,
s2,
s3 being
SortSymbol of
S st
TranslationRel S reduces s1,
s2 holds
for
t being
Translation of
A,
s1,
s2 st
S1[
t,
s1,
s2] holds
for
f being
Function st
f is_e.translation_of A,
s2,
s3 holds
S1[
f * t,
s1,
s3]
proof
let s1,
s2,
s3 be
SortSymbol of
S;
( TranslationRel S reduces s1,s2 implies for t being Translation of A,s1,s2 st S1[t,s1,s2] holds
for f being Function st f is_e.translation_of A,s2,s3 holds
S1[f * t,s1,s3] )
assume
TranslationRel S reduces s1,
s2
;
for t being Translation of A,s1,s2 st S1[t,s1,s2] holds
for f being Function st f is_e.translation_of A,s2,s3 holds
S1[f * t,s1,s3]
let t be
Translation of
A,
s1,
s2;
( S1[t,s1,s2] implies for f being Function st f is_e.translation_of A,s2,s3 holds
S1[f * t,s1,s3] )
assume A3:
for
a,
b being
set st
[a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
;
for f being Function st f is_e.translation_of A,s2,s3 holds
S1[f * t,s1,s3]
let f be
Function;
( f is_e.translation_of A,s2,s3 implies S1[f * t,s1,s3] )
assume A4:
f is_e.translation_of A,
s2,
s3
;
S1[f * t,s1,s3]
let a,
b be
set ;
( [a,b] in R . s1 implies [((f * t) . a),((f * t) . b)] in R . s3 )
assume A5:
[a,b] in R . s1
;
[((f * t) . a),((f * t) . b)] in R . s3
then reconsider a9 =
a,
b9 =
b as
Element of
A,
s1 by ZFMISC_1:87;
[(t . a9),(t . b9)] in R . s2
by A3, A5;
then A6:
[(f . (t . a9)),(f . (t . b9))] in R . s3
by A1, A4;
f . (t . a9) = (f * t) . a9
by FUNCT_2:15;
hence
[((f * t) . a),((f * t) . b)] in R . s3
by A6, FUNCT_2:15;
verum
end; A7:
for
s being
SortSymbol of
S holds
S1[
id ( the Sorts of A . s),
s,
s]
proof
let s be
SortSymbol of
S;
S1[ id ( the Sorts of A . s),s,s]let a,
b be
set ;
( [a,b] in R . s implies [((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s )
assume A8:
[a,b] in R . s
;
[((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s
then
a in the
Sorts of
A . s
by ZFMISC_1:87;
then A9:
H1(
s)
. a = a
by FUNCT_1:17;
b in the
Sorts of
A . s
by A8, ZFMISC_1:87;
hence
[((id ( the Sorts of A . s)) . a),((id ( the Sorts of A . s)) . b)] in R . s
by A8, A9, FUNCT_1:17;
verum
end; thus
for
s1,
s2 being
SortSymbol of
S st
TranslationRel S reduces s1,
s2 holds
for
t being
Translation of
A,
s1,
s2 holds
S1[
t,
s1,
s2]
from MSUALG_6:sch 1(A7, A2); verum
end;
assume A10:
for s1, s2 being SortSymbol of S st TranslationRel S reduces s1,s2 holds
for f being Translation of A,s1,s2
for a, b being set st [a,b] in R . s1 holds
[(f . a),(f . b)] in R . s2
; R is invariant
let s1, s2 be SortSymbol of S; MSUALG_6:def 8 for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
let t be Function; ( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 )
assume A11:
t is_e.translation_of A,s1,s2
; for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
then
t is Translation of A,s1,s2
by Th17;
hence
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
by A10, A11, Th17; verum