:: More on Products of Many Sorted Algebras
:: by Mariusz Giero
::
:: Received April 29, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users


registration
let I be set ;
let S be non empty non void ManySortedSign ;
let AF be MSAlgebra-Family of I,S;
cluster product AF -> non-empty ;
coherence
product AF is non-empty by MSUALG_1:def 3;
end;

registration
let X be with_non-empty_elements set ;
cluster id X -> non-empty ;
coherence
id X is non-empty ;
end;

theorem Th1: :: PRALG_3:1
for f, F being Function
for A being set st f in product F holds
f | A in product (F | A)
proof end;

theorem Th2: :: PRALG_3:2
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for a being non empty Subset of I
for Aa being MSAlgebra-Family of a,S st A | a = Aa holds
Carrier (Aa,s) = (Carrier (A,s)) | a
proof end;

theorem Th3: :: PRALG_3:3
for i being set
for I being non empty set
for EqR being Equivalence_Relation of I
for c1, c2 being Element of Class EqR st i in c1 & i in c2 holds
c1 = c2
proof end;

Lm1: for f being Function
for x being set st x in product f holds
x is Function
;

theorem :: PRALG_3:4
for D being non empty set
for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
proof end;

definition
let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let o be OperSymbol of S;
func const (o,U0) -> set equals :: PRALG_3:def 1
(Den (o,U0)) . {};
correctness
coherence
(Den (o,U0)) . {} is set ;
;
end;

:: deftheorem defines const PRALG_3:def 1 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};

theorem Th5: :: PRALG_3:5
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 = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)
proof end;

theorem :: PRALG_3:6
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for s being SortSymbol of S st the Sorts of U0 . s <> {} holds
Constants (U0,s) = { (const (o,U0)) where o is Element of the carrier' of S : ( the_result_sort_of o = s & the_arity_of o = {} ) }
proof end;

theorem Th7: :: PRALG_3:7
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 st the_arity_of o = {} holds
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))
proof end;

theorem Th8: :: PRALG_3: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 st the_arity_of o = {} holds
const (o,(product A)) in Funcs (I,(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))
proof end;

registration
let S be non empty non void ManySortedSign ;
let I be non empty set ;
let o be OperSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster const (o,(product A)) -> Relation-like Function-like ;
coherence
( const (o,(product A)) is Relation-like & const (o,(product A)) is Function-like )
proof end;
end;

theorem Th9: :: PRALG_3:9
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S st the_arity_of o = {} holds
(const (o,(product A))) . i = const (o,(A . i))
proof end;

theorem :: PRALG_3: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 the_arity_of o = {} & dom f = I & ( for i being Element of I holds f . i = const (o,(A . i)) ) holds
f = const (o,(product A))
proof end;

theorem Th11: :: PRALG_3:11
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for o being OperSymbol of S
for e being Element of Args (o,U1) st e = {} & the_arity_of o = {} & Args (o,U1) <> {} & Args (o,U2) <> {} holds
for F being ManySortedFunction of U1,U2 holds F # e = {}
proof end;

theorem Th12: :: PRALG_3:12
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) holds x in product (doms (F * (the_arity_of o)))
proof end;

theorem Th13: :: PRALG_3:13
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for n being set st n in dom (the_arity_of o) holds
(F # x) . n = (F . ((the_arity_of o) /. n)) . (x . n)
proof end;

theorem Th14: :: PRALG_3:14
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 Element of Args (o,(product A)) holds x in Funcs ((dom (the_arity_of o)),(Funcs (I,(union { ( the Sorts of (A . i9) . s9) where i9 is Element of I, s9 is Element of the carrier of S : verum } ))))
proof end;

theorem Th15: :: PRALG_3: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 Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
x . n in product (Carrier (A,((the_arity_of o) /. n)))
proof end;

theorem Th16: :: PRALG_3: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 i being Element of I
for n being set st n in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . n holds
for y being Element of Args (o,(product A))
for g being Function st g = y . n holds
g . i in the Sorts of (A . i) . s
proof end;

theorem Th17: :: PRALG_3: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 y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
commute y in product (doms (A ?. o))
proof end;

theorem Th18: :: PRALG_3: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
for y being Element of Args (o,(product A)) st the_arity_of o <> {} holds
y in dom (Commute (Frege (A ?. o)))
proof end;

theorem Th19: :: PRALG_3: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
for x being Element of Args (o,(product A)) holds (Den (o,(product A))) . x in product (Carrier (A,(the_result_sort_of o)))
proof end;

theorem Th20: :: PRALG_3:20
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra over S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . i))
proof end;

theorem Th21: :: PRALG_3:21
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for o being OperSymbol of S
for x being Element of Args (o,(product A))
for n being set st n in dom (the_arity_of o) holds
for f being Function st f = x . n holds
((commute x) . i) . n = f . i
proof end;

theorem Th22: :: PRALG_3:22
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 st the_arity_of o <> {} holds
for y being Element of Args (o,(product A))
for i9 being Element of I
for g being Function st g = (Den (o,(product A))) . y holds
g . i9 = (Den (o,(A . i9))) . ((commute y) . i9)
proof end;

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
func proj (A,i) -> ManySortedFunction of (product A),(A . i) means :Def2: :: PRALG_3:def 2
 for s being Element of S holds it . s = proj ((Carrier (A,s)),i);
existence
ex b1 being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b1 . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b2 . s = proj ((Carrier (A,s)),i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines proj PRALG_3:def 2 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for i being Element of I
for b5 being ManySortedFunction of (product A),(A . i) holds
( b5 = proj (A,i) iff for s being Element of S holds b5 . s = proj ((Carrier (A,s)),i) );

theorem Th23: :: PRALG_3:23
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 Element of Args (o,(product A)) st the_arity_of o <> {} holds
for i being Element of I holds (proj (A,i)) # x = (commute x) . i
proof end;

theorem :: PRALG_3:24
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj (A,i) is_homomorphism product A,A . i
proof end;

theorem Th25: :: PRALG_3:25
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
( F in Funcs (I,(Funcs ( the carrier of S, { ((F . i9) . s1) where s1 is SortSymbol of S, i9 is Element of I : verum } ))) & ((commute F) . s) . i = (F . i) . s )
proof end;

theorem Th26: :: PRALG_3:26
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
(commute F) . s in Funcs (I,(Funcs (( the Sorts of U1 . s),(union { ( the Sorts of (A . i9) . s1) where i9 is Element of I, s1 is SortSymbol of S : verum } ))))
proof end;

theorem Th27: :: PRALG_3:27
for I being non empty set
for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for F9 being ManySortedFunction of U1,(A . i) st F9 = F . i holds
for x being set st x in the Sorts of U1 . s holds
for f being Function st f = (commute ((commute F) . s)) . x holds
f . i = (F9 . s) . x
proof end;

theorem Th28: :: PRALG_3:28
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for s being SortSymbol of S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
for x being set st x in the Sorts of U1 . s holds
(commute ((commute F) . s)) . x in product (Carrier (A,s))
proof end;

theorem :: PRALG_3:29
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for U1 being non-empty MSAlgebra over S
for F being ManySortedFunction of I st ( for i being Element of I ex F1 being ManySortedFunction of U1,(A . i) st
( F1 = F . i & F1 is_homomorphism U1,A . i ) ) holds
ex H being ManySortedFunction of U1,(product A) st
( H is_homomorphism U1, product A & ( for i being Element of I holds (proj (A,i)) ** H = F . i ) )
proof end;

definition
let I be non empty set ;
let J be ManySortedSet of I;
let S be non empty non void ManySortedSign ;
mode MSAlgebra-Class of S,J -> ManySortedSet of I means :Def3: :: PRALG_3:def 3
 for i being set st i in I holds
it . i is MSAlgebra-Family of J . i,S;
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i is MSAlgebra-Family of J . i,S
proof end;
end;

:: deftheorem Def3 defines MSAlgebra-Class PRALG_3:def 3 :
for I being non empty set
for J being ManySortedSet of I
for S being non empty non void ManySortedSign
for b4 being ManySortedSet of I holds
( b4 is MSAlgebra-Class of S,J iff for i being set st i in I holds
b4 . i is MSAlgebra-Family of J . i,S );

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let EqR be Equivalence_Relation of I;
func A / EqR -> MSAlgebra-Class of S, id (Class EqR) means :Def4: :: PRALG_3:def 4
 for c being set st c in Class EqR holds
it . c = A | c;
existence
ex b1 being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
b1 . c = A | c
proof end;
uniqueness
for b1, b2 being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b1 . c = A | c ) & ( for c being set st c in Class EqR holds
b2 . c = A | c ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines / PRALG_3:def 4 :
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I
for b5 being MSAlgebra-Class of S, id (Class EqR) holds
( b5 = A / EqR iff for c being set st c in Class EqR holds
b5 . c = A | c );

definition
let I be non empty set ;
let S be non empty non void ManySortedSign ;
let J be V8() ManySortedSet of I;
let C be MSAlgebra-Class of S,J;
func product C -> MSAlgebra-Family of I,S means :Def5: :: PRALG_3:def 5
 for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & it . i = product Cs );
existence
ex b1 being MSAlgebra-Family of I,S st
for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs )
proof end;
uniqueness
for b1, b2 being MSAlgebra-Family of I,S st ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b1 . i = product Cs ) ) & ( for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b2 . i = product Cs ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines product PRALG_3:def 5 :
for I being non empty set
for S being non empty non void ManySortedSign
for J being V8() ManySortedSet of I
for C being MSAlgebra-Class of S,J
for b5 being MSAlgebra-Family of I,S holds
( b5 = product C iff for i being Element of I st i in I holds
ex Ji being non empty set ex Cs being MSAlgebra-Family of Ji,S st
( Ji = J . i & Cs = C . i & b5 . i = product Cs ) );

theorem :: PRALG_3:30
for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for EqR being Equivalence_Relation of I holds product A, product (product (A / EqR)) are_isomorphic
proof end;