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

begin

registration

let X be functional non empty with_common_domain set ;
cluster -> DOM X -defined Element of X;
coherence
for b₁ being Element of X holds b₁ is DOM X -defined

proof end;

end;

registration

let X be functional non empty with_common_domain set ;
cluster -> total Element of X;
coherence
for b₁ being Element of X holds b₁ is total

proof end;

end;

begin

definition

let F be Function;
canceled;
canceled;
canceled;
canceled;
canceled;
func Commute F -> Function means :Def6: :: PRALG_2:def 6
( ( for x being set 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 b₁ being Function st
( ( for x being set holds
( x in dom b₁ iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b₁ holds
b₁ . f = F . (commute f) ) )

proof end;

uniqueness
for b₁, b₂ being Function st ( for x being set holds
( x in dom b₁ iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b₁ holds
b₁ . f = F . (commute f) ) & ( for x being set holds
( x in dom b₂ iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b₂ holds
b₂ . f = F . (commute f) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem PRALG_2:def 1 :
canceled;

:: deftheorem PRALG_2:def 2 :
canceled;

:: deftheorem PRALG_2:def 3 :
canceled;

:: deftheorem PRALG_2:def 4 :
canceled;

:: deftheorem PRALG_2:def 5 :
canceled;

:: deftheorem Def6 defines Commute PRALG_2:def 6 :
for F, b₂ being Function holds
( b₂ = Commute F iff ( ( for x being set holds
( x in dom b₂ iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom b₂ holds
b₂ . f = F . (commute f) ) ) );

theorem :: PRALG_2:1

canceled;

theorem :: PRALG_2:2

canceled;

theorem :: PRALG_2:3

canceled;

theorem :: PRALG_2:4

canceled;

theorem :: PRALG_2:5

canceled;

theorem :: PRALG_2:6

canceled;

theorem :: PRALG_2:7

canceled;

theorem :: PRALG_2:8

for F being Function st dom F = {{}} holds
Commute F = F

proof end;

definition

let f be Function-yielding Function;
canceled;
:: original: Frege
redefine func Frege f -> ManySortedFunction of product (doms f) means :Def8: :: PRALG_2:def 8
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 b₁ being ManySortedFunction of product (doms f) holds
( b₁ = Frege f iff for g being Function st g in product (doms f) holds
b₁ . g = f .. g )

proof end;

end;

:: deftheorem PRALG_2:def 7 :
canceled;

:: deftheorem Def8 defines Frege PRALG_2:def 8 :
for f being Function-yielding Function
for b₂ being ManySortedFunction of product (doms f) holds
( b₂ = Frege f iff for g being Function st g in product (doms f) holds
b₂ . 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:9

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);
canceled;
func [[:f,g:]] -> Function of (([|A,B|] #) . pj),([|A,B|] . rj) means :: PRALG_2:def 10
for h being Function st h in ([|A,B|] #) . pj holds
it . h = [(f . (pr1 h)),(g . (pr2 h))];
existence
ex b₁ being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st
for h being Function st h in ([|A,B|] #) . pj holds
b₁ . h = [(f . (pr1 h)),(g . (pr2 h))]

proof end;

uniqueness
for b₁, b₂ being Function of (([|A,B|] #) . pj),([|A,B|] . rj) st ( for h being Function st h in ([|A,B|] #) . pj holds
b₁ . h = [(f . (pr1 h)),(g . (pr2 h))] ) & ( for h being Function st h in ([|A,B|] #) . pj holds
b₂ . h = [(f . (pr1 h)),(g . (pr2 h))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem PRALG_2:def 9 :
canceled;

:: deftheorem defines [[: PRALG_2:def 10 :
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 b₈ being Function of (([|A,B|] #) . pj),([|A,B|] . rj) holds
( b₈ = [[:f,g:]] iff for h being Function st h in ([|A,B|] #) . pj holds
b₈ . 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 11
for j being set 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 b₁ being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st
for j being set 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
b₁ . j = [[:f,g:]]

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r st ( for j being set 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
b₁ . j = [[:f,g:]] ) & ( for j being set 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
b₂ . j = [[:f,g:]] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines [[: PRALG_2:def 11 :
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 b₉ being ManySortedFunction of ([|A,B|] #) * p,[|A,B|] * r holds
( b₉ = [[:F,G:]] iff for j being set 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
b₉ . j = [[:f,g:]] );

begin

definition

let I be set ;
let S be non empty ManySortedSign ;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def12: :: PRALG_2:def 12
for i being set st i in I holds
it . i is non-empty MSAlgebra of S;
existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
b₁ . i is non-empty MSAlgebra of S

proof end;

end;

:: deftheorem Def12 defines MSAlgebra-Family PRALG_2:def 12 :
for I being set
for S being non empty ManySortedSign
for b₃ being ManySortedSet of I holds
( b₃ is MSAlgebra-Family of I,S iff for i being set st i in I holds
b₃ . i is non-empty MSAlgebra of 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 of S;
coherence
A . i is non-empty MSAlgebra of S by Def12;

end;

definition

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

end;

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

registration

let S be non empty ManySortedSign ;
let U1 be non-empty MSAlgebra of 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 14
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 14 :
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;

begin

theorem Th10: :: PRALG_2:10

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 Th11: :: PRALG_2:11

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 of S;
func [:U1,U2:] -> MSAlgebra of S equals :: PRALG_2:def 15
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 of S ;

end;

:: deftheorem defines [: PRALG_2:def 15 :
for S being non empty ManySortedSign
for U1, U2 being non-empty MSAlgebra of 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 of 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 :Def16: :: PRALG_2:def 16
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b₁ being ManySortedSet of I st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₁ . i = the Sorts of U0 . s ) ) & ( not I <> {} implies ex b₁ being ManySortedSet of I st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₁ . i = the Sorts of U0 . s ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₂ . i = the Sorts of U0 . s ) ) implies b₁ = b₂ ) & ( not I <> {} & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being ManySortedSet of I holds verum;
;

end;

:: deftheorem Def16 defines Carrier PRALG_2:def 16 :
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 b₅ being ManySortedSet of I holds
( ( I <> {} implies ( b₅ = Carrier (A,s) iff for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₅ . i = the Sorts of U0 . s ) ) ) & ( not I <> {} implies ( b₅ = Carrier (A,s) iff b₅ = {} ) ) );

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 :Def17: :: PRALG_2:def 17
for s being SortSymbol of S holds it . s = product (Carrier (A,s));
existence
ex b₁ being ManySortedSet of the carrier of S st
for s being SortSymbol of S holds b₁ . s = product (Carrier (A,s))

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of the carrier of S st ( for s being SortSymbol of S holds b₁ . s = product (Carrier (A,s)) ) & ( for s being SortSymbol of S holds b₂ . s = product (Carrier (A,s)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines SORTS PRALG_2:def 17 :
for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S
for b₄ being ManySortedSet of the carrier of S holds
( b₄ = SORTS A iff for s being SortSymbol of S holds b₄ . 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 :Def18: :: PRALG_2:def 18
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Charact of U0 ) if I <> {}
otherwise it = {} ;
existence
( ( I <> {} implies ex b₁ being ManySortedFunction of I st
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₁ . i = the Charact of U0 ) ) & ( not I <> {} implies ex b₁ being ManySortedFunction of I st b₁ = {} ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of I holds
( ( I <> {} & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₁ . i = the Charact of U0 ) ) & ( for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & b₂ . i = the Charact of U0 ) ) implies b₁ = b₂ ) & ( not I <> {} & b₁ = {} & b₂ = {} implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being ManySortedFunction of I holds verum;
;

end;

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

theorem Th12: :: PRALG_2:12

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 Th13: :: PRALG_2:13

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 19
(commute (OPER A)) . o;
coherence
(commute (OPER A)) . o is ManySortedFunction of I

proof end;

end;

:: deftheorem defines ?. PRALG_2:def 19 :
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 Th14: :: PRALG_2:14

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:15

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 Th16: :: PRALG_2:16

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 Th17: :: PRALG_2:17

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 Th18: :: PRALG_2:18

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 20
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 b₁ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st
for o being OperSymbol of S holds b₁ . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( not I <> {} implies ex b₁ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S st verum ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} & ( for o being OperSymbol of S holds b₁ . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) & ( for o being OperSymbol of S holds b₂ . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) implies b₁ = b₂ ) & ( not I <> {} implies b₁ = b₂ ) )

proof end;

correctness
consistency
for b₁ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds verum;
;

end;

:: deftheorem defines OPS PRALG_2:def 20 :
for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for b₄ being ManySortedFunction of ((SORTS A) #) * the Arity of S,(SORTS A) * the ResultSort of S holds
( ( I <> {} implies ( b₄ = OPS A iff for o being OperSymbol of S holds b₄ . o = IFEQ ((the_arity_of o),{},(commute (A ?. o)),(Commute (Frege (A ?. o)))) ) ) & ( not I <> {} implies ( b₄ = 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 of S equals :: PRALG_2:def 21
MSAlgebra(# (SORTS A),(OPS A) #);
coherence
MSAlgebra(# (SORTS A),(OPS A) #) is MSAlgebra of S ;

end;

:: deftheorem defines product PRALG_2:def 21 :
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:19

canceled;

theorem :: PRALG_2:20

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 ) ;