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

begin

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

end;

registration

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

proof end;

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

canceled;

theorem :: PRALG_3:5

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;

begin

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra of 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 of S
for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};

theorem Th6: :: PRALG_3:6

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 = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)

proof end;

theorem :: PRALG_3:7

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of 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 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
(commute (OPER A)) . o in Funcs (I,(Funcs ({{}},(union { (Result (o,(A . i9))) where i9 is Element of I : verum } ))))

proof end;

theorem Th9: :: PRALG_3: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 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 Th10: :: PRALG_3:10

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: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
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 Th12: :: PRALG_3:12

for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of 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;

begin

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 of 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 Th14: :: PRALG_3:14

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2 being non-empty MSAlgebra of 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 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)) 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 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 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 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 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 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
commute y in product (doms (A ?. o))

proof end;

theorem Th19: :: PRALG_3:19

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 Th20: :: PRALG_3:20

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 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 st the_arity_of o <> {} holds
for U1 being non-empty MSAlgebra of S
for x being Element of Args (o,(product A)) holds (commute x) . i is Element of Args (o,(A . 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 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 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 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;

begin

definition

let I be non empty set ;
let S be non empty non void ManySortedSign ;
canceled;
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 :Def3: :: PRALG_3:def 3
for s being Element of S holds it . s = proj ((Carrier (A,s)),i);
existence
ex b₁ being ManySortedFunction of (product A),(A . i) st
for s being Element of S holds b₁ . s = proj ((Carrier (A,s)),i)

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (product A),(A . i) st ( for s being Element of S holds b₁ . s = proj ((Carrier (A,s)),i) ) & ( for s being Element of S holds b₂ . s = proj ((Carrier (A,s)),i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem PRALG_3:def 2 :
canceled;

:: deftheorem Def3 defines proj PRALG_3:def 3 :
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 b₅ being ManySortedFunction of (product A),(A . i) holds
( b₅ = proj (A,i) iff for s being Element of S holds b₅ . s = proj ((Carrier (A,s)),i) );

theorem Th24: :: PRALG_3:24

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: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 holds proj (A,i) is_homomorphism product A,A . i

proof end;

theorem Th26: :: PRALG_3:26

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 of 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 Th27: :: PRALG_3:27

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 of 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 Th28: :: PRALG_3:28

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 of 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 Th29: :: 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 s being SortSymbol of S
for U1 being non-empty MSAlgebra of 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:30

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

begin

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 :Def4: :: PRALG_3:def 4
for i being set st i in I holds
it . i is MSAlgebra-Family of J . i,S;
existence
ex b₁ being ManySortedSet of I st
for i being set st i in I holds
b₁ . i is MSAlgebra-Family of J . i,S

proof end;

end;

:: deftheorem Def4 defines MSAlgebra-Class PRALG_3:def 4 :
for I being non empty set
for J being ManySortedSet of I
for S being non empty non void ManySortedSign
for b₄ being ManySortedSet of I holds
( b₄ is MSAlgebra-Class of S,J iff for i being set st i in I holds
b₄ . 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 :Def5: :: PRALG_3:def 5
for c being set st c in Class EqR holds
it . c = A | c;
existence
ex b₁ being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
b₁ . c = A | c

proof end;

uniqueness
for b₁, b₂ being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b₁ . c = A | c ) & ( for c being set st c in Class EqR holds
b₂ . c = A | c ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines / PRALG_3:def 5 :
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 b₅ being MSAlgebra-Class of S, id (Class EqR) holds
( b₅ = A / EqR iff for c being set st c in Class EqR holds
b₅ . 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 :Def6: :: PRALG_3:def 6
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 b₁ 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 & b₁ . i = product Cs )

proof end;

uniqueness
for b₁, b₂ 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 & b₁ . 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 & b₂ . i = product Cs ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines product PRALG_3:def 6 :
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 b₅ being MSAlgebra-Family of I,S holds
( b₅ = 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 & b₅ . i = product Cs ) );

theorem :: PRALG_3:31

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;