let U0, U1, U2 be Universal_Algebra; :: thesis: ( U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2 )
assume A1:
( U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 )
; :: thesis: U0 is SubAlgebra of U2
then A2:
the carrier of U0 is Subset of U1
by Def8;
the carrier of U1 is Subset of U2
by A1, Def8;
hence
the carrier of U0 is Subset of U2
by A2, XBOOLE_1:1; :: according to UNIALG_2:def 8 :: thesis: 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 )
reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1, Def8;
reconsider B2 = the carrier of U1 as non empty Subset of U2 by A1, Def8;
let B be non empty Subset of U2; :: thesis: ( B = the carrier of U0 implies ( the charact of U0 = Opers U2,B & B is opers_closed ) )
assume A3:
B = the carrier of U0
; :: thesis: ( the charact of U0 = Opers U2,B & B is opers_closed )
then A4:
B = B1
;
A5:
( the charact of U0 = Opers U1,B1 & B1 is opers_closed )
by A1, Def8;
A6:
( the charact of U1 = Opers U2,B2 & B2 is opers_closed )
by A1, Def8;
A7:
now let o2 be
operation of
U2;
:: thesis: B is_closed_on o2A8:
B2 is_closed_on o2
by A6, Def5;
consider n being
Nat such that A9:
(
n in dom the
charact of
U2 & the
charact of
U2 . n = o2 )
by FINSEQ_2:11;
A10:
dom the
charact of
U2 = dom (Opers U2,B2)
by Def7;
then reconsider o21 = the
charact of
U1 . n as
operation of
U1 by A6, A9, FUNCT_1:def 5;
A11:
B1 is_closed_on o21
by A5, Def5;
A12:
o21 = o2 /. B2
by A6, A9, A10, Def7;
A13:
dom the
charact of
U1 = dom (Opers U1,B1)
by Def7;
then reconsider o20 = the
charact of
U0 . n as
operation of
U0 by A5, A6, A9, A10, FUNCT_1:def 5;
A14:
o20 = o21 /. B1
by A5, A6, A9, A10, A13, Def7;
A15:
(
dom o20 = (arity o20) -tuples_on the
carrier of
U0 &
dom o21 = (arity o21) -tuples_on the
carrier of
U1 &
dom o2 = (arity o2) -tuples_on the
carrier of
U2 )
by Th2;
A16:
(
o20 = o21 | ((arity o21) -tuples_on B1) &
o21 = o2 | ((arity o2) -tuples_on B2) )
by A8, A11, A12, A14, Def6;
then
(arity o20) -tuples_on B1 = ((arity o21) -tuples_on the carrier of U1) /\ ((arity o21) -tuples_on B1)
by A15, RELAT_1:90;
then A17:
arity o20 = arity o21
by Th1, FINSEQ_2:130;
dom (o2 | ((arity o2) -tuples_on B2)) = (dom o2) /\ ((arity o2) -tuples_on B2)
by RELAT_1:90;
then A18:
arity o2 = arity o21
by A15, A16, Th1, FINSEQ_2:130;
now let s be
FinSequence of
B;
:: thesis: ( len s = arity o2 implies o2 . s in B )reconsider s0 =
s as
Element of the
carrier of
U0 * by A3, FINSEQ_1:def 11;
reconsider s1 =
s as
Element of
B1 * by A3, FINSEQ_1:def 11;
(
rng s c= B &
B c= B2 )
by A2, A3, FINSEQ_1:def 4;
then
rng s c= B2
by 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 A19:
len s = arity o2
;
:: thesis: o2 . s in Bthen
s1 in { w where w is Element of B1 * : len w = arity o21 }
by A18;
then A20:
s1 in (arity o21) -tuples_on B1
by FINSEQ_2:def 4;
s2 in { w where w is Element of B2 * : len w = arity o2 }
by A19;
then A21:
s2 in (arity o2) -tuples_on B2
by FINSEQ_2:def 4;
A22:
o20 . s0 =
(o21 | ((arity o21) -tuples_on B1)) . s1
by A11, A14, Def6
.=
o21 . s1
by A20, FUNCT_1:72
.=
(o2 | ((arity o2) -tuples_on B2)) . s2
by A8, A12, Def6
.=
o2 . s
by A21, FUNCT_1:72
;
s0 in { w where w is Element of the carrier of U0 * : len w = arity o20 }
by A17, A18, A19;
then
s0 in (arity o20) -tuples_on the
carrier of
U0
by FINSEQ_2:def 4;
then
(
o20 . s0 in rng o20 &
rng o20 c= B )
by A3, A15, FUNCT_1:def 5, RELAT_1:def 19;
hence
o2 . s in B
by A22;
:: thesis: verum end; hence
B is_closed_on o2
by Def4;
:: thesis: verum end;
A23: dom the charact of U0 =
dom (Opers U1,B1)
by A1, Def8
.=
dom the charact of U1
by Def7
;
A24: dom the charact of U1 =
dom (Opers U2,B2)
by A1, Def8
.=
dom the charact of U2
by Def7
;
A25:
dom the charact of U2 = dom (Opers U2,B)
by Def7;
now let n be
Nat;
:: thesis: ( n in dom (Opers U2,B) implies (Opers U2,B) . n = the charact of U0 . n )assume A26:
n in dom (Opers U2,B)
;
:: thesis: (Opers U2,B) . n = the charact of U0 . nthen reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A25, FUNCT_1:def 5;
reconsider o21 = the
charact of
U1 . n as
operation of
U1 by A24, A25, A26, FUNCT_1:def 5;
A27:
B2 is_closed_on o2
by A6, Def5;
A28:
B1 is_closed_on o21
by A5, Def5;
thus (Opers U2,B) . n =
o2 /. B
by A26, Def7
.=
o2 | ((arity o2) -tuples_on B)
by A7, Def6
.=
o2 | (((arity o2) -tuples_on B2) /\ ((arity o2) -tuples_on B))
by A4, Th1
.=
(o2 | ((arity o2) -tuples_on B2)) | ((arity o2) -tuples_on B)
by RELAT_1:100
.=
(o2 /. B2) | ((arity o2) -tuples_on B)
by A27, Def6
.=
o21 | ((arity o2) -tuples_on B)
by A6, A24, A25, A26, Def7
.=
o21 | ((arity o21) -tuples_on B1)
by A1, A3, A24, A25, A26, Th9
.=
o21 /. B1
by A28, Def6
.=
the
charact of
U0 . n
by A5, A23, A24, A25, A26, Def7
;
:: thesis: verum end;
hence
the charact of U0 = Opers U2,B
by A23, A24, A25, FINSEQ_1:17; :: thesis: B is opers_closed
thus
B is opers_closed
by A7, Def5; :: thesis: verum