:: MSUALG_9 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: MSUALG_9:sch 1
MSSExD{ F1() -> non empty set , P1[ set , set ] } :
ex f being ManySortedSet of F1() st
for i being Element of F1() holds P1[i,f . i]
provided
A1: for i being Element of F1() ex j being set st P1[i,j]
proof end;

registration
let I be set ;
let M be ManySortedSet of I;
cluster locally-finite Element of Bool M;
existence
ex b1 being Element of Bool M st b1 is locally-finite
proof end;
end;

registration
let I be set ;
let M be V2 ManySortedSet of I;
cluster V2 locally-finite ManySortedSubset of M;
existence
ex b1 being ManySortedSubset of M st
( b1 is non-empty & b1 is locally-finite )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let o be OperSymbol of S;
cluster -> FinSequence-like Element of Args o,A;
coherence
for b1 being Element of Args o,A holds b1 is FinSequence-like
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let I be set ;
let s be SortSymbol of S;
let F be MSAlgebra-Family of I,S;
cluster -> Relation-like Function-like Element of (SORTS F) . s;
coherence
for b1 being Element of (SORTS F) . s holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2 ManySortedSet of the carrier of S;
cluster FreeGen X -> V2 free ;
coherence
( FreeGen X is free & FreeGen X is non-empty )
by MSAFREE:15, MSAFREE:17;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V2 ManySortedSet of the carrier of S;
cluster FreeMSA X -> free ;
coherence
FreeMSA X is free
by MSAFREE:18;
end;

registration
let S be non empty non void ManySortedSign ;
let A, B be non-empty MSAlgebra of S;
cluster [:A,B:] -> non-empty ;
coherence
[:A,B:] is non-empty
proof end;
end;

theorem :: MSUALG_9:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, X, Y being set
for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
proof end;

theorem Th2: :: MSUALG_9:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for Y being set
for f being Function of X,{Y} holds rng f = {Y}
proof end;

theorem Th3: :: MSUALG_9:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty finite set ex f being Function of NAT ,A st rng f = A
proof end;

theorem Th4: :: MSUALG_9:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set holds Class (nabla I) c= {I}
proof end;

theorem Th5: :: MSUALG_9:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty set holds Class (nabla I) = {I}
proof end;

theorem Th6: :: MSUALG_9:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, a being set ex A being ManySortedSet of I st {A} = I --> {a}
proof end;

theorem :: MSUALG_9:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I ex B being V2 ManySortedSet of I st A c= B
proof end;

theorem :: MSUALG_9:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for M being V2 ManySortedSet of I
for B being locally-finite ManySortedSubset of M ex C being V2 locally-finite ManySortedSubset of M st B c= C
proof end;

theorem :: MSUALG_9:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, B being ManySortedSet of I
for F, G being ManySortedFunction of A,{B} holds F = G
proof end;

theorem Th10: :: MSUALG_9:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being V2 ManySortedSet of I
for B being ManySortedSet of I
for F being ManySortedFunction of A,{B} holds F is "onto"
proof end;

theorem Th11: :: MSUALG_9:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for B being V2 ManySortedSet of I
for F being ManySortedFunction of {A},B holds F is "1-1"
proof end;

theorem :: MSUALG_9:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for X being V2 ManySortedSet of the carrier of S holds Reverse X is "1-1"
proof end;

theorem :: MSUALG_9:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being V2 locally-finite ManySortedSet of I ex F being ManySortedFunction of I --> NAT ,A st F is "onto"
proof end;

theorem :: MSUALG_9:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for f, g being Element of product the Sorts of A st ( for i being set holds (proj the Sorts of A,i) . f = (proj the Sorts of A,i) . g ) holds
f = g
proof end;

theorem :: MSUALG_9:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for I being non empty set
for s being Element of S
for A being MSAlgebra-Family of I,S
for f, g being Element of product (Carrier A,s) st ( for a being Element of I holds (proj (Carrier A,s),a) . f = (proj (Carrier A,s),a) . g ) holds
f = g
proof end;

theorem :: MSUALG_9:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra of S
for C being non-empty MSSubAlgebra of A
for h1 being ManySortedFunction of B,C st h1 is_homomorphism B,C holds
for h2 being ManySortedFunction of B,A st h1 = h2 holds
h2 is_homomorphism B,A
proof end;

theorem :: MSUALG_9:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra of S
for F being ManySortedFunction of A,B st F is_monomorphism A,B holds
A, Image F are_isomorphic
proof end;

theorem Th18: :: MSUALG_9:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra of S
for F being ManySortedFunction of A,B st F is "onto" holds
for o being OperSymbol of S
for x being Element of Args o,B ex y being Element of Args o,A st F # y = x
proof end;

theorem Th19: :: MSUALG_9:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for o being OperSymbol of S
for x being Element of Args o,A holds (Den o,A) . x in the Sorts of A . (the_result_sort_of o)
proof end;

theorem Th20: :: MSUALG_9:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B, C being non-empty MSAlgebra of S
for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
proof end;

definition
let I be set ;
let A be ManySortedSet of I;
let B, C be V2 ManySortedSet of I;
let F be ManySortedFunction of A,[|B,C|];
func Mpr1 F -> ManySortedFunction of A,B means :Def1: :: MSUALG_9:def 1
for i being set st i in I holds
it . i = pr1 (F . i);
existence
ex b1 being ManySortedFunction of A,B st
for i being set st i in I holds
b1 . i = pr1 (F . i)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of A,B st ( for i being set st i in I holds
b1 . i = pr1 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr1 (F . i) ) holds
b1 = b2
proof end;
func Mpr2 F -> ManySortedFunction of A,C means :Def2: :: MSUALG_9:def 2
for i being set st i in I holds
it . i = pr2 (F . i);
existence
ex b1 being ManySortedFunction of A,C st
for i being set st i in I holds
b1 . i = pr2 (F . i)
proof end;
uniqueness
for b1, b2 being ManySortedFunction of A,C st ( for i being set st i in I holds
b1 . i = pr2 (F . i) ) & ( for i being set st i in I holds
b2 . i = pr2 (F . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Mpr1 MSUALG_9:def 1 :
for I being set
for A being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,B holds
( b6 = Mpr1 F iff for i being set st i in I holds
b6 . i = pr1 (F . i) );

:: deftheorem Def2 defines Mpr2 MSUALG_9:def 2 :
for I being set
for A being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|]
for b6 being ManySortedFunction of A,C holds
( b6 = Mpr2 F iff for i being set st i in I holds
b6 . i = pr2 (F . i) );

theorem :: MSUALG_9:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, a being set
for A being ManySortedSet of I
for F being ManySortedFunction of A,[|(I --> {a}),(I --> {a})|] holds Mpr1 F = Mpr2 F
proof end;

theorem :: MSUALG_9:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr1 F is "onto"
proof end;

theorem :: MSUALG_9:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st F is "onto" holds
Mpr2 F is "onto"
proof end;

theorem :: MSUALG_9:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A, M being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for F being ManySortedFunction of A,[|B,C|] st M in doms F holds
for i being set st i in I holds
(F .. M) . i = [(((Mpr1 F) .. M) . i),(((Mpr2 F) .. M) . i)]
proof end;

registration
let S be non empty ManySortedSign ;
cluster the Sorts of (Trivial_Algebra S) -> V2 locally-finite ;
coherence
( the Sorts of (Trivial_Algebra S) is locally-finite & the Sorts of (Trivial_Algebra S) is non-empty )
proof end;
end;

registration
let S be non empty ManySortedSign ;
cluster Trivial_Algebra S -> non-empty locally-finite ;
coherence
( Trivial_Algebra S is locally-finite & Trivial_Algebra S is non-empty )
proof end;
end;

theorem Th25: :: MSUALG_9:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args o,A holds
( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
proof end;

theorem Th26: :: MSUALG_9:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
proof end;

theorem :: MSUALG_9:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being MSAlgebra of S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds
A, Trivial_Algebra S are_isomorphic
proof end;

theorem :: MSUALG_9:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C being MSCongruence of A holds C is ManySortedSubset of [|the Sorts of A,the Sorts of A|]
proof end;

theorem :: MSUALG_9:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for R being Subset of (CongrLatt A)
for F being SubsetFamily of [|the Sorts of A,the Sorts of A|] st R = F holds
meet |:F:| is MSCongruence of A
proof end;

theorem :: MSUALG_9:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C being MSCongruence of A st C = [|the Sorts of A,the Sorts of A|] holds
the Sorts of (QuotMSAlg A,C) = {the Sorts of A}
proof end;

theorem Th31: :: MSUALG_9:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra of S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
(MSHomQuot F) ** (MSNat_Hom A,(MSCng F)) = F
proof end;

theorem Th32: :: MSUALG_9:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg A,C) . s ex x being Element of the Sorts of A . s st a = Class C,x
proof end;

theorem :: MSUALG_9:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
proof end;

theorem :: MSUALG_9:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom A,C) . s) . x = ((MSNat_Hom A,C) . s) . y iff [x,y] in C . s )
proof end;

Lm1: now
let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto"

let A be non-empty MSAlgebra of S; :: thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto"

let C1, C2 be MSCongruence of A; :: thesis: for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is "onto"

let G be ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2); :: thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) implies G is "onto" )

assume A1: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ; :: thesis: G is "onto"
thus G is "onto" :: thesis: verum
proof
set sL = the Sorts of (QuotMSAlg A,C1);
set sP = the Sorts of (QuotMSAlg A,C2);
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in the carrier of S or rng (G . i) = the Sorts of (QuotMSAlg A,C2) . i )
assume i in the carrier of S ; :: thesis: rng (G . i) = the Sorts of (QuotMSAlg A,C2) . i
then reconsider s = i as SortSymbol of S ;
rng (G . s) c= the Sorts of (QuotMSAlg A,C2) . s by RELSET_1:12;
hence rng (G . i) c= the Sorts of (QuotMSAlg A,C2) . i ; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (QuotMSAlg A,C2) . i c= rng (G . i)
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in the Sorts of (QuotMSAlg A,C2) . i or q in rng (G . i) )
assume A2: q in the Sorts of (QuotMSAlg A,C2) . i ; :: thesis: q in rng (G . i)
q in Class (C2 . s) by A2, MSUALG_4:def 8;
then consider a being set such that
A3: a in the Sorts of A . s and
A4: q = Class (C2 . s),a by EQREL_1:def 5;
reconsider a = a as Element of the Sorts of A . s by A3;
A5: dom (G . s) = the Sorts of (QuotMSAlg A,C1) . s by FUNCT_2:def 1;
Class (C1 . s),a in Class (C1 . s) by EQREL_1:def 5;
then Class C1,a in Class (C1 . s) ;
then reconsider x = Class C1,a as Element of the Sorts of (QuotMSAlg A,C1) . s by MSUALG_4:def 8;
(G . s) . x = Class C2,a by A1
.= Class (C2 . s),a ;
hence q in rng (G . i) by A4, A5, FUNCT_1:def 5; :: thesis: verum
end;
end;

theorem Th35: :: MSUALG_9:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G ** (MSNat_Hom A,C1) = MSNat_Hom A,C2
proof end;

theorem Th36: :: MSUALG_9:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2
proof end;

theorem :: MSUALG_9:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra of S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg A,C1),B st
( H is_homomorphism QuotMSAlg A,C1,B & F = H ** (MSNat_Hom A,C1) )
proof end;