let V be set ; for C being finite set
for K being Element of SubstitutionSet V,C holds FinJoin K,(Atom V,C) = FinUnion K,(singleton (PFuncs V,C))
let C be finite set ; for K being Element of SubstitutionSet V,C holds FinJoin K,(Atom V,C) = FinUnion K,(singleton (PFuncs V,C))
let K be Element of SubstitutionSet V,C; FinJoin K,(Atom V,C) = FinUnion K,(singleton (PFuncs V,C))
A1:
the L_join of (SubstLatt V,C) is commutative
;
deffunc H1( Element of Fin (PFuncs V,C)) -> Element of SubstitutionSet V,C = mi $1;
A2:
the L_join of (SubstLatt V,C) is associative
;
A3:
FinUnion K,(singleton (PFuncs V,C)) c= mi (FinUnion K,(singleton (PFuncs V,C)))
proof
let a be
set ;
TARSKI:def 3 ( not a in FinUnion K,(singleton (PFuncs V,C)) or a in mi (FinUnion K,(singleton (PFuncs V,C))) )
assume A4:
a in FinUnion K,
(singleton (PFuncs V,C))
;
a in mi (FinUnion K,(singleton (PFuncs V,C)))
then consider b being
Element of
PFuncs V,
C such that A5:
b in K
and A6:
a in (singleton (PFuncs V,C)) . b
by SETWISEO:70;
A7:
a = b
by A6, SETWISEO:68;
A8:
now
K in SubstitutionSet V,
C
;
then
K in { A where A is Element of Fin (PFuncs V,C) : ( ( for u being set st u in A holds
u is finite ) & ( for s, t being Element of PFuncs V,C st s in A & t in A & s c= t holds
s = t ) ) }
by SUBSTLAT:def 1;
then A9:
ex
AA being
Element of
Fin (PFuncs V,C) st
(
K = AA & ( for
u being
set st
u in AA holds
u is
finite ) & ( for
s,
t being
Element of
PFuncs V,
C st
s in AA &
t in AA &
s c= t holds
s = t ) )
;
let s be
finite set ;
( s in FinUnion K,(singleton (PFuncs V,C)) & s c= a implies s = a )assume that A10:
s in FinUnion K,
(singleton (PFuncs V,C))
and A11:
s c= a
;
s = aconsider t being
Element of
PFuncs V,
C such that A12:
t in K
and A13:
s in (singleton (PFuncs V,C)) . t
by A10, SETWISEO:70;
s = t
by A13, SETWISEO:68;
hence
s = a
by A5, A7, A11, A12, A9;
verum end;
a is
finite
by A5, A7, Th2;
hence
a in mi (FinUnion K,(singleton (PFuncs V,C)))
by A4, A8, SUBSTLAT:7;
verum
end;
consider g being Function of (Fin (PFuncs V,C)),(SubstitutionSet V,C) such that
A14:
for B being Element of Fin (PFuncs V,C) holds g . B = H1(B)
from FUNCT_2:sch 4();
reconsider g = g as Function of (Fin (PFuncs V,C)),the carrier of (SubstLatt V,C) by SUBSTLAT:def 4;
A15:
the L_join of (SubstLatt V,C) is idempotent
;
A19:
now let a be
set ;
( a in K implies ((g * (singleton (PFuncs V,C))) | K) . a = ((Atom V,C) | K) . a )assume A20:
a in K
;
((g * (singleton (PFuncs V,C))) | K) . a = ((Atom V,C) | K) . athen reconsider a9 =
a as
Element of
PFuncs V,
C by SETWISEO:14;
A21:
a9 is
finite
by A20, Th2;
then reconsider KL =
{a9} as
Element of
SubstitutionSet V,
C by Th6;
thus ((g * (singleton (PFuncs V,C))) | K) . a =
(g * (singleton (PFuncs V,C))) . a
by A20, FUNCT_1:72
.=
g . ((singleton (PFuncs V,C)) . a9)
by FUNCT_2:21
.=
g . {a}
by SETWISEO:67
.=
mi KL
by A14
.=
KL
by SUBSTLAT:11
.=
(Atom V,C) . a9
by A21, Lm7
.=
((Atom V,C) | K) . a
by A20, FUNCT_1:72
;
verum end;
A22:
mi (FinUnion K,(singleton (PFuncs V,C))) c= FinUnion K,(singleton (PFuncs V,C))
by SUBSTLAT:8;
A23:
rng (singleton (PFuncs V,C)) c= Fin (PFuncs V,C)
;
A24:
K c= PFuncs V,C
by FINSUB_1:def 5;
then
K c= dom (Atom V,C)
by FUNCT_2:def 1;
then A25:
dom ((Atom V,C) | K) = K
by RELAT_1:91;
reconsider gs = g * (singleton (PFuncs V,C)) as Function of (PFuncs V,C),the carrier of (SubstLatt V,C) ;
A26: g . ({}. (PFuncs V,C)) =
mi ({}. (PFuncs V,C))
by A14
.=
{}
by SUBSTLAT:9
.=
Bottom (SubstLatt V,C)
by SUBSTLAT:26
.=
the_unity_wrt the L_join of (SubstLatt V,C)
by LATTICE2:28
;
dom g = Fin (PFuncs V,C)
by FUNCT_2:def 1;
then A27:
dom (g * (singleton (PFuncs V,C))) = dom (singleton (PFuncs V,C))
by A23, RELAT_1:46;
dom (singleton (PFuncs V,C)) = PFuncs V,C
by FUNCT_2:def 1;
then
dom ((g * (singleton (PFuncs V,C))) | K) = K
by A24, A27, RELAT_1:91;
hence FinJoin K,(Atom V,C) =
FinJoin K,gs
by A25, A19, FUNCT_1:9, LATTICE2:69
.=
the L_join of (SubstLatt V,C) $$ K,gs
by LATTICE2:def 3
.=
g . (FinUnion K,(singleton (PFuncs V,C)))
by A1, A2, A15, A26, A16, SETWISEO:65
.=
mi (FinUnion K,(singleton (PFuncs V,C)))
by A14
.=
FinUnion K,(singleton (PFuncs V,C))
by A22, A3, XBOOLE_0:def 10
;
verum