:: Products of Many Sorted Algebras
:: by Beata Madras
::
:: Received April 25, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users


::
:: Preliminaries
::
registration
let X be functional non empty with_common_domain set ;
cluster -> DOM X -defined for Element of X;
coherence
for b1 being Element of X holds b1 is DOM X -defined
proof end;
end;

registration
let X be functional non empty with_common_domain set ;
cluster -> total for Element of X;
coherence
for b1 being Element of X holds b1 is total
proof end;
end;

:: Operations on Functions
definition
let F be Function;
func Commute F -> Function means :Def1: :: PRALG_2:def 1
( ( for x being object holds
( x in dom it iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds
it . f = F . (commute f) ) );
existence
ex b1 being Function st
( ( for x being object holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) )
proof end;
uniqueness
for b1, b2 being Function st ( for x being object holds
( x in dom b1 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b1 holds
b1 . f = F . (commute f) ) & ( for x being object holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Commute PRALG_2:def 1 :
for F, b2 being Function holds
( b2 = Commute F iff ( ( for x being object holds
( x in dom b2 iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b2 holds
b2 . f = F . (commute f) ) ) );

theorem :: PRALG_2:1
for F being Function st dom F = {{}} holds
Commute F = F
proof end;

definition
let f be Function-yielding Function;
:: original: Frege
redefine func Frege f -> ManySortedFunction of product (doms f) means :Def2: :: PRALG_2:def 2
 for g being Function st g in product (doms f) holds
it . g = f .. g;
coherence
Frege f is ManySortedFunction of product (doms f)
proof end;
compatibility
for b1 being ManySortedFunction of product (doms f) holds
( b1 = Frege f iff for g being Function st g in product (doms f) holds
b1 . g = f .. g )
proof end;
end;

:: deftheorem Def2 defines Frege PRALG_2:def 2 :
for f being Function-yielding Function
for b2 being ManySortedFunction of product (doms f) holds
( b2 = Frege f iff for g being Function st g in product (doms f) holds
b2 . g = f .. g );

registration
let I be set ;
let A, B be V2() ManySortedSet of I;
cluster [|A,B|] -> V2() ;
coherence
[|A,B|] is non-empty
proof end;
end;

theorem :: PRALG_2:2
for I being non empty set
for J being set
for A, B being ManySortedSet of I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
proof end;

definition
let I be non empty set ;
let A, B be V2() ManySortedSet of I;
let pj be Element of I * ;
let rj be Element of I;
let f be Function of ((A #) . pj),(A . rj);
let g be Function of ((B #) . pj),(B . rj);
func [[:f,g:]] -> Function of (([|A,B|] #) . pj),([|A,B|] . rj) means :: PRALG_2:def 3
 for h being Function st h in ([|A,B|] #) . pj holds
it . h = [(f . (pr1 h)),(g . (pr2 h))];
existence
ex b1 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st
for h being Function st h in ([|A,B|] #) . pj holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))]
proof end;
uniqueness
for b1, b2 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st ( for h being Function st h in ([|A,B|] #) . pj holds
b1 . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds
b2 . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines [[: PRALG_2:def 3 :
for I being non empty set
for A, B being V2() ManySortedSet of I
for pj being Element of I *
for rj being Element of I
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj)
for b8 being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds
( b8 = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds
b8 . h = [(f . (pr1 h)),(g . (pr2 h))] );

definition
let I be non empty set ;
let J be set ;
let A, B be V2() ManySortedSet of I;
let p be Function of J,(I *);
let r be Function of J,I;
let F be ManySortedFunction of (A #) * p,A * r;
let G be ManySortedFunction of (B #) * p,B * r;
func [[:F,G:]] -> ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r means :: PRALG_2:def 4
 for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
it . j = [[:f,g:]];
existence
ex b1 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st
for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b1 . j = [[:f,g:]]
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st ( for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b1 . j = [[:f,g:]] ) & ( for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b2 . j = [[:f,g:]] ) holds
b1 = b2
proof end;
end;

:: deftheorem defines [[: PRALG_2:def 4 :
for I being non empty set
for J being set
for A, B being V2() ManySortedSet of I
for p being Function of J,(I *)
for r being Function of J,I
for F being ManySortedFunction of (A #) * p,A * r
for G being ManySortedFunction of (B #) * p,B * r
for b9 being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds
( b9 = [[:F,G:]] iff for j being object st j in J holds
for pj being Element of I *
for rj being Element of I st pj = p . j & rj = r . j holds
for f being Function of ((A #) . pj),(A . rj)
for g being Function of ((B #) . pj),(B . rj) st f = F . j & g = G . j holds
b9 . j = [[:f,g:]] );

::
:: Family of Many Sorted Universal Algebras
::
definition
let I be set ;
let S be non empty ManySortedSign ;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def5: :: PRALG_2:def 5
 for i being object st i in I holds
it . i is non-empty MSAlgebra over S;
existence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
b1 . i is non-empty MSAlgebra over S
proof end;
end;

:: deftheorem Def5 defines MSAlgebra-Family PRALG_2:def 5 :
for I being set
for S being non empty ManySortedSign
for b3 being ManySortedSet of I holds
( b3 is MSAlgebra-Family of I,S iff for i being object st i in I holds
b3 . i is non-empty MSAlgebra over S );

definition
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
:: original: .
redefine func A . i -> non-empty MSAlgebra over S;
coherence
A . i is non-empty MSAlgebra over S by Def5;
end;

definition
let S be non empty ManySortedSign ;
let U1 be MSAlgebra over S;
func |.U1.| -> set equals :: PRALG_2:def 6
 union (rng the Sorts of U1);
coherence
union (rng the Sorts of U1) is set ;
end;

:: deftheorem defines |. PRALG_2:def 6 :
for S being non empty ManySortedSign
for U1 being MSAlgebra over S holds |.U1.| = union (rng the Sorts of U1);

registration
let S be non empty ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
cluster |.U1.| -> non empty ;
coherence
not |.U1.| is empty
proof end;
end;

definition
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func |.A.| -> set equals :: PRALG_2:def 7
 union { |.(A . i).| where i is Element of I : verum } ;
coherence
union { |.(A . i).| where i is Element of I : verum } is set ;
end;

:: deftheorem defines |. PRALG_2:def 7 :
for I being non empty set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds |.A.| = union { |.(A . i).| where i is Element of I : verum } ;

registration
let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster |.A.| -> non empty ;
coherence
not |.A.| is empty
proof end;
end;

::
:: Product of Many Sorted Universal Algebras
::
theorem Th3: :: PRALG_2:3
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds
( Args (o,U0) = product ( the Sorts of U0 * (the_arity_of o)) & dom ( the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result (o,U0) = the Sorts of U0 . (the_result_sort_of o) )
proof end;

theorem Th4: :: PRALG_2:4
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} holds
Args (o,U0) = {{}}
proof end;

definition
let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
func [:U1,U2:] -> MSAlgebra over S equals :: PRALG_2:def 8
 MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);
coherence
MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #) is MSAlgebra over S ;
end;

:: deftheorem defines [: PRALG_2:def 8 :
for S being non empty ManySortedSign
for U1, U2 being non-empty MSAlgebra over S holds [:U1,U2:] = MSAlgebra(# [| the Sorts of U1, the Sorts of U2|],[[: the Charact of U1, the Charact of U2:]] #);

registration
let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
cluster [:U1,U2:] -> strict ;
coherence
[:U1,U2:] is strict ;
end;

definition
let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
func Carrier (A,s) -> ManySortedSet of I means :Def9: :: PRALG_2:def 9
 for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b1 being ManySortedSet of I st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b2 . i = the Sorts of U0 . s ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedSet of I holds verum;
;
end;

:: deftheorem Def9 defines Carrier PRALG_2:def 9 :
for I being set
for S being non empty ManySortedSign
for s being SortSymbol of S
for A being MSAlgebra-Family of I,S
for b5 being ManySortedSet of I holds
( ( I <> {} implies ( b5 = Carrier (A,s) iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b5 . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b5 = Carrier (A,s) iff b5 = {} ) ) );

registration
let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster Carrier (A,s) -> V2() ;
coherence
Carrier (A,s) is non-empty
proof end;
end;

definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func SORTS A -> ManySortedSet of the carrier of S means :Def10: :: PRALG_2:def 10
 for s being SortSymbol of S holds it . s = product (Carrier (A,s));
existence
ex b1 being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b1 . s = product (Carrier (A,s))
proof end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b1 . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds b2 . s = product (Carrier (A,s)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines SORTS PRALG_2:def 10 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedSet of the carrier of S holds
( b4 = SORTS A iff for s being SortSymbol of S holds b4 . s = product (Carrier (A,s)) );

registration
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster SORTS A -> V2() ;
coherence
SORTS A is non-empty
proof end;
end;

definition
let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPER A -> ManySortedFunction of I means :Def11: :: PRALG_2:def 11
 for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & it . i = the Charact of U0 ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b1 being ManySortedFunction of I st
for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( not I <> {} implies ex b1 being ManySortedFunction of I st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b1 . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b2 . i = the Charact of U0 ) ) implies b1 = b2 ) & ( not I <> {} & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedFunction of I holds verum;
;
end;

:: deftheorem Def11 defines OPER PRALG_2:def 11 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of I holds
( ( I <> {} implies ( b4 = OPER A iff for i being set st i in I holds
ex U0 being MSAlgebra over S st
( U0 = A . i & b4 . i = the Charact of U0 ) ) ) & ( not I <> {} implies ( b4 = OPER A iff b4 = {} ) ) );

theorem Th5: :: PRALG_2:5
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I, the carrier' of S:]
proof end;

theorem Th6: :: PRALG_2:6
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (OPER A))))))
proof end;

definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let o be OperSymbol of S;
func A ?. o -> ManySortedFunction of I equals :: PRALG_2:def 12
(commute (OPER A)) . o;
coherence
(commute (OPER A)) . o is ManySortedFunction of I
proof end;
end;

:: deftheorem defines ?. PRALG_2:def 12 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds A ?. o = (commute (OPER A)) . o;

theorem Th7: :: PRALG_2:7
for I being non empty set
for i being Element of I
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den (o,(A . i))
proof end;

theorem :: PRALG_2:8
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function
proof end;

theorem Th9: :: PRALG_2:9
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result (o,(A . i)) ) )
proof end;

theorem Th10: :: PRALG_2:10
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args (o,(A . i)) ) & rng f c= Funcs ((dom (the_arity_of o)),|.A.|) )
proof end;

theorem Th11: :: PRALG_2:11
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args (o,(A . i)) ) )
proof end;

definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPS A -> ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S means :: PRALG_2:def 13
 for o being OperSymbol of S holds it . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) if I <> {}
otherwise verum;
existence
( ( I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( not I <> {} implies ex b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} & ( for o being OperSymbol of S holds b1 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds b2 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies b1 = b2 ) & ( not I <> {} implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds verum;
;
end;

:: deftheorem defines OPS PRALG_2:def 13 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for b4 being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} implies ( b4 = OPS A iff for o being OperSymbol of S holds b4 . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b4 = OPS A iff verum ) ) );

definition
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func product A -> MSAlgebra over S equals :: PRALG_2:def 14
 MSAlgebra(# (SORTS A),(OPS A) #);
coherence
MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra over S ;
end;

:: deftheorem defines product PRALG_2:def 14 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds product A = MSAlgebra(# (SORTS A),(OPS A) #);

registration
let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster product A -> strict ;
coherence
product A is strict ;
end;

theorem :: PRALG_2:12
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds
( the Sorts of (product A) = SORTS A & the Charact of (product A) = OPS A ) ;