let U0, U1, U2 be Universal_Algebra; ( U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2 )
assume that
A1:
U0 is SubAlgebra of U1
and
A2:
U1 is SubAlgebra of U2
; U0 is SubAlgebra of U2
A3:
the carrier of U0 is Subset of U1
by A1, Def7;
reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2, Def7;
A4:
the charact of U1 = Opers (U2,B2)
by A2, Def7;
the carrier of U1 is Subset of U2
by A2, Def7;
hence
the carrier of U0 is Subset of U2
by A3, XBOOLE_1:1; UNIALG_2:def 7 for B being non empty Subset of U2 st B = the carrier of U0 holds
( the charact of U0 = Opers (U2,B) & B is opers_closed )
let B be non empty Subset of U2; ( B = the carrier of U0 implies ( the charact of U0 = Opers (U2,B) & B is opers_closed ) )
assume A5:
B = the carrier of U0
; ( the charact of U0 = Opers (U2,B) & B is opers_closed )
reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1, Def7;
A6:
the charact of U0 = Opers (U1,B1)
by A1, Def7;
A7:
B2 is opers_closed
by A2, Def7;
A8: dom the charact of U1 =
dom (Opers (U2,B2))
by A2, Def7
.=
dom the charact of U2
by Def6
;
A9:
B1 is opers_closed
by A1, Def7;
A10:
now for o2 being operation of U2 holds B is_closed_on o2let o2 be
operation of
U2;
B is_closed_on o2consider n being
Nat such that A11:
n in dom the
charact of
U2
and A12:
the
charact of
U2 . n = o2
by FINSEQ_2:10;
A13:
dom the
charact of
U2 = dom (Opers (U2,B2))
by Def6;
then reconsider o21 = the
charact of
U1 . n as
operation of
U1 by A4, A11, FUNCT_1:def 3;
A14:
dom o21 = (arity o21) -tuples_on the
carrier of
U1
by MARGREL1:22;
A15:
dom the
charact of
U1 = dom (Opers (U1,B1))
by Def6;
then reconsider o20 = the
charact of
U0 . n as
operation of
U0 by A6, A4, A11, A13, FUNCT_1:def 3;
A16:
dom o20 = (arity o20) -tuples_on the
carrier of
U0
by MARGREL1:22;
A17:
(
dom o2 = (arity o2) -tuples_on the
carrier of
U2 &
dom (o2 | ((arity o2) -tuples_on B2)) = (dom o2) /\ ((arity o2) -tuples_on B2) )
by MARGREL1:22, RELAT_1:61;
A18:
B2 is_closed_on o2
by A7;
A19:
o21 = o2 /. B2
by A4, A11, A12, A13, Def6;
then
o21 = o2 | ((arity o2) -tuples_on B2)
by A18, Def5;
then A20:
arity o2 = arity o21
by A14, A17, FINSEQ_2:110, MARGREL1:21;
A21:
B1 is_closed_on o21
by A9;
A22:
o20 = o21 /. B1
by A6, A4, A11, A13, A15, Def6;
then
o20 = o21 | ((arity o21) -tuples_on B1)
by A21, Def5;
then
(arity o20) -tuples_on B1 = ((arity o21) -tuples_on the carrier of U1) /\ ((arity o21) -tuples_on B1)
by A16, A14, RELAT_1:61;
then A23:
arity o20 = arity o21
by FINSEQ_2:110, MARGREL1:21;
now for s being FinSequence of B st len s = arity o2 holds
o2 . s in Blet s be
FinSequence of
B;
( len s = arity o2 implies o2 . s in B )reconsider s1 =
s as
Element of
B1 * by A5, FINSEQ_1:def 11;
reconsider s0 =
s as
Element of the
carrier of
U0 * by A5, FINSEQ_1:def 11;
A24:
rng o20 c= B
by A5, RELAT_1:def 19;
rng s c= B
by FINSEQ_1:def 4;
then
rng s c= B2
by A3, A5, XBOOLE_1:1;
then
s is
FinSequence of
B2
by FINSEQ_1:def 4;
then reconsider s2 =
s as
Element of
B2 * by FINSEQ_1:def 11;
assume A25:
len s = arity o2
;
o2 . s in Bthen
s2 in { w where w is Element of B2 * : len w = arity o2 }
;
then A26:
s2 in (arity o2) -tuples_on B2
by FINSEQ_2:def 4;
s0 in { w where w is Element of the carrier of U0 * : len w = arity o20 }
by A23, A20, A25;
then
s0 in (arity o20) -tuples_on the
carrier of
U0
by FINSEQ_2:def 4;
then A27:
o20 . s0 in rng o20
by A16, FUNCT_1:def 3;
s1 in { w where w is Element of B1 * : len w = arity o21 }
by A20, A25;
then A28:
s1 in (arity o21) -tuples_on B1
by FINSEQ_2:def 4;
o20 . s0 =
(o21 | ((arity o21) -tuples_on B1)) . s1
by A21, A22, Def5
.=
o21 . s1
by A28, FUNCT_1:49
.=
(o2 | ((arity o2) -tuples_on B2)) . s2
by A18, A19, Def5
.=
o2 . s
by A26, FUNCT_1:49
;
hence
o2 . s in B
by A27, A24;
verum end; hence
B is_closed_on o2
;
verum end;
A29: dom the charact of U0 =
dom (Opers (U1,B1))
by A1, Def7
.=
dom the charact of U1
by Def6
;
A30:
dom the charact of U2 = dom (Opers (U2,B))
by Def6;
A31:
B = B1
by A5;
now for n being Nat st n in dom (Opers (U2,B)) holds
(Opers (U2,B)) . n = the charact of U0 . nlet n be
Nat;
( n in dom (Opers (U2,B)) implies (Opers (U2,B)) . n = the charact of U0 . n )assume A32:
n in dom (Opers (U2,B))
;
(Opers (U2,B)) . n = the charact of U0 . nthen reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A30, FUNCT_1:def 3;
reconsider o21 = the
charact of
U1 . n as
operation of
U1 by A8, A30, A32, FUNCT_1:def 3;
A33:
B2 is_closed_on o2
by A7;
A34:
B1 is_closed_on o21
by A9;
thus (Opers (U2,B)) . n =
o2 /. B
by A32, Def6
.=
o2 | ((arity o2) -tuples_on B)
by A10, Def5
.=
o2 | (((arity o2) -tuples_on B2) /\ ((arity o2) -tuples_on B))
by A31, MARGREL1:21
.=
(o2 | ((arity o2) -tuples_on B2)) | ((arity o2) -tuples_on B)
by RELAT_1:71
.=
(o2 /. B2) | ((arity o2) -tuples_on B)
by A33, Def5
.=
o21 | ((arity o2) -tuples_on B)
by A4, A8, A30, A32, Def6
.=
o21 | ((arity o21) -tuples_on B1)
by A2, A5, A8, A30, A32, Th6
.=
o21 /. B1
by A34, Def5
.=
the
charact of
U0 . n
by A6, A29, A8, A30, A32, Def6
;
verum end;
hence
the charact of U0 = Opers (U2,B)
by A29, A8, A30, FINSEQ_1:13; B is opers_closed
thus
B is opers_closed
by A10; verum