let U1, U2, U3, U4 be Universal_Algebra; ( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar implies [:U1,U3:] is SubAlgebra of [:U2,U4:] )
assume that
A1:
U1 is SubAlgebra of U2
and
A2:
U3 is SubAlgebra of U4
and
A3:
U2,U4 are_similar
; [:U1,U3:] is SubAlgebra of [:U2,U4:]
A4:
[:U2,U4:] = UAStr(# [: the carrier of U2, the carrier of U4:],(Opers (U2,U4)) #)
by A3, Def5;
A5:
U1,U2 are_similar
by A1, UNIALG_2:13;
then A6:
U1,U4 are_similar
by A3;
A7:
U3,U4 are_similar
by A2, UNIALG_2:13;
then A8:
[:U1,U3:] = UAStr(# [: the carrier of U1, the carrier of U3:],(Opers (U1,U3)) #)
by A6, Def5, UNIALG_2:2;
A9:
( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 )
by A1, A2, UNIALG_2:def 7;
hence
the carrier of [:U1,U3:] is Subset of [:U2,U4:]
by A8, A4, ZFMISC_1:96; UNIALG_2:def 7 for b1 being Element of bool the carrier of [:U2,U4:] holds
( not b1 = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],b1) & b1 is opers_closed ) )
let B be non empty Subset of [:U2,U4:]; ( not B = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed ) )
assume A10:
B = the carrier of [:U1,U3:]
; ( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed )
len the charact of U4 = len (signature U2)
by UNIALG_1:def 4, A3;
then A11:
( dom the charact of U4 = Seg (len the charact of U4) & len the charact of U4 = len the charact of U2 )
by FINSEQ_1:def 3, UNIALG_1:def 4;
A12:
dom the charact of U1 = Seg (len the charact of U1)
by FINSEQ_1:def 3;
A13:
dom the charact of U2 = Seg (len the charact of U2)
by FINSEQ_1:def 3;
A14:
U1,U3 are_similar
by A7, A6;
then A15:
len the charact of [:U1,U3:] = len the charact of U1
by A8, Def4;
len the charact of U1 = len (signature U3)
by UNIALG_1:def 4, A14;
then A16:
( dom the charact of U3 = Seg (len the charact of U3) & len the charact of U1 = len the charact of U3 )
by FINSEQ_1:def 3, UNIALG_1:def 4;
A17:
dom (Opers ([:U2,U4:],B)) = Seg (len (Opers ([:U2,U4:],B)))
by FINSEQ_1:def 3;
A18:
dom the charact of [:U2,U4:] = dom (Opers ([:U2,U4:],B))
by UNIALG_2:def 6;
then
len the charact of [:U2,U4:] = len (Opers ([:U2,U4:],B))
by FINSEQ_3:29;
then A19:
len the charact of U2 = len (Opers ([:U2,U4:],B))
by A3, A4, Def4;
len the charact of U1 = len (signature U2)
by UNIALG_1:def 4, A5;
then A20:
len the charact of [:U1,U3:] = len (Opers ([:U2,U4:],B))
by A19, A15, UNIALG_1:def 4;
reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def 7;
A21:
B3 is opers_closed
by A2, UNIALG_2:def 7;
reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 7;
A22:
B1 is opers_closed
by A1, UNIALG_2:def 7;
A23:
[: the carrier of U1, the carrier of U3:] c= [: the carrier of U2, the carrier of U4:]
by A9, ZFMISC_1:96;
A24:
for o being operation of [:U2,U4:] holds B is_closed_on o
proof
let o be
operation of
[:U2,U4:];
B is_closed_on olet s be
FinSequence of
B;
UNIALG_2:def 3 ( not len s = arity o or o . s in B )
reconsider s0 =
s as
Element of
[: the carrier of U1, the carrier of U3:] * by A8, A10, FINSEQ_1:def 11;
consider n being
Nat such that A25:
n in dom the
charact of
[:U2,U4:]
and A26:
the
charact of
[:U2,U4:] . n = o
by FINSEQ_2:10;
reconsider s3 =
pr2 s0 as
Element of
B3 * by FINSEQ_1:def 11;
reconsider s1 =
pr1 s0 as
Element of
B1 * by FINSEQ_1:def 11;
A27:
len the
charact of
[:U2,U4:] = len the
charact of
U2
by A3, A4, Def4;
A28:
n in Seg (len the charact of [:U2,U4:])
by A25, FINSEQ_1:def 3;
then A29:
n in dom the
charact of
U2
by A27, FINSEQ_1:def 3;
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by FUNCT_1:def 3;
len the
charact of
U4 = len the
charact of
U2
by A3, UNIALG_2:1;
then
n in dom the
charact of
U4
by A28, A27, FINSEQ_1:def 3;
then reconsider o4 = the
charact of
U4 . n as
operation of
U4 by FUNCT_1:def 3;
A30:
o = [[:o2,o4:]]
by A3, A26, A29, Th5;
o4 = the
charact of
U4 . n
;
then A31:
arity o = arity o2
by A3, A26, A29, Th5;
rng s0 c= [: the carrier of U1, the carrier of U3:]
by FINSEQ_1:def 4;
then
rng s0 c= [: the carrier of U2, the carrier of U4:]
by A23;
then
s0 is
FinSequence of
[: the carrier of U2, the carrier of U4:]
by FINSEQ_1:def 4;
then reconsider ss =
s0 as
Element of
[: the carrier of U2, the carrier of U4:] * by FINSEQ_1:def 11;
o2 = the
charact of
U2 . n
;
then A32:
arity o = arity o4
by A3, A26, A29, Th5;
assume A33:
len s = arity o
;
o . s in B
then A34:
ss in { w where w is Element of [: the carrier of U2, the carrier of U4:] * : len w = arity o2 }
by A31;
(
B3 is_closed_on o4 &
len s3 = len s0 )
by A21, Def2;
then A35:
o4 . s3 in B3
by A33, A32;
(
B1 is_closed_on o2 &
len s1 = len s0 )
by A22, Def1;
then A36:
o2 . s1 in B1
by A33, A31;
dom [[:o2,o4:]] = (arity o2) -tuples_on [: the carrier of U2, the carrier of U4:]
by A31, A32, Def3;
then
o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))]
by A31, A32, A30, A34, Def3;
hence
o . s in B
by A8, A10, A36, A35, ZFMISC_1:87;
verum
end;
A37:
dom the charact of U4 = dom (Opers (U4,B3))
by UNIALG_2:def 6;
A38:
dom the charact of [:U1,U3:] = Seg (len the charact of [:U1,U3:])
by FINSEQ_1:def 3;
A39:
dom the charact of U2 = dom (Opers (U2,B1))
by UNIALG_2:def 6;
for n being Nat st n in dom the charact of [:U1,U3:] holds
the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
proof
let n be
Nat;
( n in dom the charact of [:U1,U3:] implies the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n )
assume A40:
n in dom the
charact of
[:U1,U3:]
;
the charact of [:U1,U3:] . n = (Opers ([:U2,U4:],B)) . n
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A19, A20, A13, A38, FUNCT_1:def 3;
reconsider o4 = the
charact of
U4 . n as
operation of
U4 by A19, A20, A38, A11, A40, FUNCT_1:def 3;
reconsider o24 = the
charact of
[:U2,U4:] . n as
operation of
[:U2,U4:] by A18, A20, A38, A17, A40, FUNCT_1:def 3;
A41:
o24 = [[:o2,o4:]]
by A3, A19, A20, A13, A38, A40, Th5;
reconsider o3 = the
charact of
U3 . n as
operation of
U3 by A15, A38, A16, A40, FUNCT_1:def 3;
(Opers (U4,B3)) . n = o4 /. B3
by A19, A20, A38, A11, A37, A40, UNIALG_2:def 6;
then A42:
o3 = o4 /. B3
by A2, UNIALG_2:def 7;
o2 = the
charact of
U2 . n
;
then A43:
arity o24 = arity o4
by A3, A19, A20, A13, A38, A40, Th5;
reconsider o1 = the
charact of
U1 . n as
operation of
U1 by A15, A12, A38, A40, FUNCT_1:def 3;
(Opers (U2,B1)) . n = o2 /. B1
by A19, A20, A13, A38, A39, A40, UNIALG_2:def 6;
then A44:
o1 = o2 /. B1
by A1, UNIALG_2:def 7;
A45:
B3 is_closed_on o4
by A21;
then A46:
arity (o4 /. B3) = arity o4
by UNIALG_2:5;
o4 = the
charact of
U4 . n
;
then A47:
arity o24 = arity o2
by A3, A19, A20, A13, A38, A40, Th5;
then A48:
dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) =
(dom [[:o2,o4:]]) /\ ((arity o2) -tuples_on B)
by RELAT_1:61
.=
((arity o2) -tuples_on the carrier of [:U2,U4:]) /\ ((arity o2) -tuples_on B)
by A4, A43, A47, Def3
.=
(arity o2) -tuples_on B
by MARGREL1:21
;
A49:
B1 is_closed_on o2
by A22;
then A50:
arity (o2 /. B1) = arity o2
by UNIALG_2:5;
then A51:
dom [[:(o2 /. B1),(o4 /. B3):]] = (arity o2) -tuples_on B
by A8, A10, A43, A47, A46, Def3;
A52:
now for x being object st x in (arity o2) -tuples_on B holds
[[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . xlet x be
object ;
( x in (arity o2) -tuples_on B implies [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x )A53:
dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) c= dom [[:o2,o4:]]
by RELAT_1:60;
assume A54:
x in (arity o2) -tuples_on B
;
[[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . xthen consider s being
Element of
B * such that A55:
s = x
and A56:
len s = arity o2
;
rng s c= B
by FINSEQ_1:def 4;
then
rng s c= [: the carrier of U2, the carrier of U4:]
by A4, XBOOLE_1:1;
then reconsider s0 =
s as
FinSequence of
[: the carrier of U2, the carrier of U4:] by FINSEQ_1:def 4;
A57:
([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x =
[[:o2,o4:]] . s0
by A48, A54, A55, FUNCT_1:47
.=
[(o2 . (pr1 s0)),(o4 . (pr2 s0))]
by A43, A47, A48, A54, A55, A53, Def3
;
reconsider s1 =
s as
FinSequence of
[:B1,B3:] by A8, A10;
reconsider s11 =
pr1 s1 as
Element of
B1 * by FINSEQ_1:def 11;
len (pr1 s1) = len s1
by Def1;
then A58:
s11 in { a where a is Element of B1 * : len a = arity o2 }
by A56;
reconsider s12 =
pr2 s1 as
Element of
B3 * by FINSEQ_1:def 11;
len (pr2 s1) = len s1
by Def2;
then A59:
s12 in { b where b is Element of B3 * : len b = arity o4 }
by A43, A47, A56;
A60:
dom (o4 | ((arity o4) -tuples_on B3)) =
(dom o4) /\ ((arity o4) -tuples_on B3)
by RELAT_1:61
.=
((arity o4) -tuples_on the carrier of U4) /\ ((arity o4) -tuples_on B3)
by MARGREL1:22
.=
(arity o4) -tuples_on B3
by MARGREL1:21
;
A61:
dom (o2 | ((arity o2) -tuples_on B1)) =
(dom o2) /\ ((arity o2) -tuples_on B1)
by RELAT_1:61
.=
((arity o2) -tuples_on the carrier of U2) /\ ((arity o2) -tuples_on B1)
by MARGREL1:22
.=
(arity o2) -tuples_on B1
by MARGREL1:21
;
[[:(o2 /. B1),(o4 /. B3):]] . x =
[((o2 /. B1) . (pr1 s1)),((o4 /. B3) . (pr2 s1))]
by A43, A47, A50, A46, A51, A54, A55, Def3
.=
[((o2 | ((arity o2) -tuples_on B1)) . s11),((o4 /. B3) . (pr2 s1))]
by A49, UNIALG_2:def 5
.=
[(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))]
by A58, A61, FUNCT_1:47
.=
[(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))]
by A45, UNIALG_2:def 5
.=
[(o2 . (pr1 s1)),(o4 . (pr2 s1))]
by A59, A60, FUNCT_1:47
;
hence
[[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x
by A57;
verum end;
thus (Opers ([:U2,U4:],B)) . n =
o24 /. B
by A20, A38, A17, A40, UNIALG_2:def 6
.=
[[:o2,o4:]] | ((arity o24) -tuples_on B)
by A24, A41, UNIALG_2:def 5
.=
[[:(o2 /. B1),(o4 /. B3):]]
by A51, A48, A52
.=
the
charact of
[:U1,U3:] . n
by A14, A8, A40, A44, A42, Def4
;
verum
end;
hence
( the charact of [:U1,U3:] = Opers ([:U2,U4:],B) & B is opers_closed )
by A24, A20, FINSEQ_2:9; verum