let U1, U2, U3, U4 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar implies [:U1,U3:] is SubAlgebra of [:U2,U4:] )
assume A1:
( U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar )
; :: thesis: [:U1,U3:] is SubAlgebra of [:U2,U4:]
then A2:
( U1,U2 are_similar & U3,U4 are_similar )
by UNIALG_2:16;
then A3:
U1,U4 are_similar
by A1, UNIALG_2:4;
then A4:
U1,U3 are_similar
by A2, UNIALG_2:4;
A5:
( [:U1,U3:] = UAStr(# [:the carrier of U1,the carrier of U3:],(Opers U1,U3) #) & [:U2,U4:] = UAStr(# [:the carrier of U2,the carrier of U4:],(Opers U2,U4) #) )
by A2, A3, Def5, UNIALG_2:4;
A6:
( the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 )
by A1, UNIALG_2:def 8;
then A7:
[:the carrier of U1,the carrier of U3:] c= [:the carrier of U2,the carrier of U4:]
by ZFMISC_1:119;
thus
the carrier of [:U1,U3:] is Subset of [:U2,U4:]
by A5, A6, ZFMISC_1:119; :: according to UNIALG_2:def 8 :: thesis: 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:]; :: thesis: ( not B = the carrier of [:U1,U3:] or ( the charact of [:U1,U3:] = Opers [:U2,U4:],B & B is opers_closed ) )
assume A8:
B = the carrier of [:U1,U3:]
; :: thesis: ( the charact of [:U1,U3:] = Opers [:U2,U4:],B & B is opers_closed )
reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 8;
reconsider B3 = the carrier of U3 as non empty Subset of U4 by A1, UNIALG_2:def 8;
A9:
( B1 is opers_closed & B3 is opers_closed )
by A1, UNIALG_2:def 8;
A10:
for o being operation of [:U2,U4:] holds B is_closed_on o
proof
let o be
operation of
[:U2,U4:];
:: thesis: B is_closed_on olet s be
FinSequence of
B;
:: according to UNIALG_2:def 4 :: thesis: ( not len s = arity o or o . s in B )
assume A11:
len s = arity o
;
:: thesis: o . s in B
reconsider s0 =
s as
Element of
[:the carrier of U1,the carrier of U3:] * by A5, A8, FINSEQ_1:def 11;
consider n being
Nat such that A12:
(
n in dom the
charact of
[:U2,U4:] & the
charact of
[:U2,U4:] . n = o )
by FINSEQ_2:11;
A13:
(
n in Seg (len the charact of [:U2,U4:]) & the
charact of
[:U2,U4:] . n = o )
by A12, FINSEQ_1:def 3;
A14:
len the
charact of
[:U2,U4:] = len the
charact of
U2
by A1, A5, Def4;
then A15:
n in dom the
charact of
U2
by A13, FINSEQ_1:def 3;
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by FUNCT_1:def 5;
len the
charact of
U4 = len the
charact of
U2
by A1, UNIALG_2:3;
then
n in dom the
charact of
U4
by A13, A14, FINSEQ_1:def 3;
then reconsider o4 = the
charact of
U4 . n as
operation of
U4 by FUNCT_1:def 5;
(
o2 = the
charact of
U2 . n &
o4 = the
charact of
U4 . n )
;
then A16:
(
arity o = arity o2 &
arity o = arity o4 &
o = [[:o2,o4:]] )
by A1, A12, A15, Th6;
then A17:
dom [[:o2,o4:]] = (arity o2) -tuples_on [:the carrier of U2,the carrier of U4:]
by Def3;
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 A7, XBOOLE_1:1;
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;
A18:
ss in { w where w is Element of [:the carrier of U2,the carrier of U4:] * : len w = arity o2 }
by A11, A16;
reconsider s1 =
pr1 s0 as
Element of
B1 * by FINSEQ_1:def 11;
reconsider s3 =
pr2 s0 as
Element of
B3 * by FINSEQ_1:def 11;
A19:
(
B1 is_closed_on o2 &
B3 is_closed_on o4 )
by A9, UNIALG_2:def 5;
(
len s1 = len s0 &
len s3 = len s0 )
by Def1, Def2;
then A20:
(
o2 . s1 in B1 &
o4 . s3 in B3 )
by A11, A16, A19, UNIALG_2:def 4;
o . s = [(o2 . (pr1 ss)),(o4 . (pr2 ss))]
by A16, A17, A18, Def3;
hence
o . s in B
by A5, A8, A20, ZFMISC_1:106;
:: thesis: verum
end;
A21:
dom the charact of [:U2,U4:] = dom (Opers [:U2,U4:],B)
by UNIALG_2:def 7;
then
len the charact of [:U2,U4:] = len (Opers [:U2,U4:],B)
by FINSEQ_3:31;
then A22:
len the charact of U2 = len (Opers [:U2,U4:],B)
by A1, A5, Def4;
A23:
len the charact of [:U1,U3:] = len the charact of U1
by A4, A5, Def4;
signature U1 = signature U2
by A2, UNIALG_2:def 2;
then
len the charact of U1 = len (signature U2)
by UNIALG_1:def 11;
then A24:
len the charact of [:U1,U3:] = len (Opers [:U2,U4:],B)
by A22, A23, UNIALG_1:def 11;
A25:
( dom the charact of U1 = Seg (len the charact of U1) & dom the charact of U2 = Seg (len the charact of U2) & dom the charact of U3 = Seg (len the charact of U3) & dom the charact of U4 = Seg (len the charact of U4) & dom the charact of [:U1,U3:] = Seg (len the charact of [:U1,U3:]) & dom the charact of [:U2,U4:] = Seg (len the charact of [:U2,U4:]) & dom (Opers [:U2,U4:],B) = Seg (len (Opers [:U2,U4:],B)) & dom (Opers U2,B1) = Seg (len (Opers U2,B1)) & dom (Opers U4,B3) = Seg (len (Opers U4,B3)) )
by FINSEQ_1:def 3;
signature U4 = signature U2
by A1, UNIALG_2:def 2;
then
len the charact of U4 = len (signature U2)
by UNIALG_1:def 11;
then A26:
len the charact of U4 = len the charact of U2
by UNIALG_1:def 11;
signature U1 = signature U3
by A4, UNIALG_2:def 2;
then
len the charact of U1 = len (signature U3)
by UNIALG_1:def 11;
then A27:
len the charact of U1 = len the charact of U3
by UNIALG_1:def 11;
A28:
dom the charact of U2 = dom (Opers U2,B1)
by UNIALG_2:def 7;
A29:
dom the charact of U4 = dom (Opers U4,B3)
by UNIALG_2:def 7;
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;
:: thesis: ( n in dom the charact of [:U1,U3:] implies the charact of [:U1,U3:] . n = (Opers [:U2,U4:],B) . n )
assume A30:
n in dom the
charact of
[:U1,U3:]
;
:: thesis: the charact of [:U1,U3:] . n = (Opers [:U2,U4:],B) . n
then reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A22, A24, A25, FUNCT_1:def 5;
reconsider o4 = the
charact of
U4 . n as
operation of
U4 by A22, A24, A25, A26, A30, FUNCT_1:def 5;
reconsider o24 = the
charact of
[:U2,U4:] . n as
operation of
[:U2,U4:] by A21, A24, A25, A30, FUNCT_1:def 5;
reconsider o1 = the
charact of
U1 . n as
operation of
U1 by A23, A25, A30, FUNCT_1:def 5;
reconsider o3 = the
charact of
U3 . n as
operation of
U3 by A23, A25, A27, A30, FUNCT_1:def 5;
(
o2 = the
charact of
U2 . n &
o4 = the
charact of
U4 . n )
;
then A31:
(
o24 = [[:o2,o4:]] &
arity o24 = arity o4 &
arity o24 = arity o2 )
by A1, A22, A24, A25, A30, Th6;
A32:
(Opers U2,B1) . n = o2 /. B1
by A22, A24, A25, A28, A30, UNIALG_2:def 7;
A33:
(Opers U4,B3) . n = o4 /. B3
by A22, A24, A25, A26, A29, A30, UNIALG_2:def 7;
A34:
o1 = o2 /. B1
by A1, A32, UNIALG_2:def 8;
A35:
o3 = o4 /. B3
by A1, A33, UNIALG_2:def 8;
A36:
(
B is_closed_on o24 &
B1 is_closed_on o2 &
B3 is_closed_on o4 )
by A9, A10, UNIALG_2:def 5;
then A37:
(
arity (o2 /. B1) = arity o2 &
arity (o4 /. B3) = arity o4 )
by UNIALG_2:8;
then A38:
dom [[:(o2 /. B1),(o4 /. B3):]] = (arity o2) -tuples_on B
by A5, A8, A31, Def3;
A39:
dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) =
(dom [[:o2,o4:]]) /\ ((arity o2) -tuples_on B)
by A31, RELAT_1:90
.=
((arity o2) -tuples_on the carrier of [:U2,U4:]) /\ ((arity o2) -tuples_on B)
by A5, A31, Def3
.=
(arity o2) -tuples_on B
by UNIALG_2:1
;
A40:
now let x be
set ;
:: thesis: ( x in (arity o2) -tuples_on B implies [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x )assume A41:
x in (arity o2) -tuples_on B
;
:: thesis: [[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . xthen consider s being
Element of
B * such that A42:
(
s = x &
len s = arity o2 )
;
(
B c= [:the carrier of U2,the carrier of U4:] &
rng s c= B )
by A5, FINSEQ_1:def 4;
then
rng s c= [:the carrier of U2,the carrier of U4:]
by XBOOLE_1:1;
then reconsider s0 =
s as
FinSequence of
[:the carrier of U2,the carrier of U4:] by FINSEQ_1:def 4;
A43:
dom ([[:o2,o4:]] | ((arity o24) -tuples_on B)) c= dom [[:o2,o4:]]
by RELAT_1:89;
A44:
([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x =
[[:o2,o4:]] . s0
by A39, A41, A42, FUNCT_1:70
.=
[(o2 . (pr1 s0)),(o4 . (pr2 s0))]
by A31, A39, A41, A42, A43, Def3
;
reconsider s1 =
s as
FinSequence of
[:B1,B3:] by A5, A8;
reconsider s11 =
pr1 s1 as
Element of
B1 * by FINSEQ_1:def 11;
reconsider s12 =
pr2 s1 as
Element of
B3 * by FINSEQ_1:def 11;
(
len (pr1 s1) = len s1 &
len (pr1 s0) = len s0 )
by Def1;
then A45:
s11 in { a where a is Element of B1 * : len a = arity o2 }
by A42;
A46:
dom (o2 | ((arity o2) -tuples_on B1)) =
(dom o2) /\ ((arity o2) -tuples_on B1)
by RELAT_1:90
.=
((arity o2) -tuples_on the carrier of U2) /\ ((arity o2) -tuples_on B1)
by UNIALG_2:2
.=
(arity o2) -tuples_on B1
by UNIALG_2:1
;
(
len (pr2 s1) = len s1 &
len (pr2 s0) = len s0 )
by Def2;
then A47:
s12 in { b where b is Element of B3 * : len b = arity o4 }
by A31, A42;
A48:
dom (o4 | ((arity o4) -tuples_on B3)) =
(dom o4) /\ ((arity o4) -tuples_on B3)
by RELAT_1:90
.=
((arity o4) -tuples_on the carrier of U4) /\ ((arity o4) -tuples_on B3)
by UNIALG_2:2
.=
(arity o4) -tuples_on B3
by UNIALG_2:1
;
[[:(o2 /. B1),(o4 /. B3):]] . x =
[((o2 /. B1) . (pr1 s1)),((o4 /. B3) . (pr2 s1))]
by A31, A37, A38, A41, A42, Def3
.=
[((o2 | ((arity o2) -tuples_on B1)) . s11),((o4 /. B3) . (pr2 s1))]
by A36, UNIALG_2:def 6
.=
[(o2 . (pr1 s1)),((o4 /. B3) . (pr2 s1))]
by A45, A46, FUNCT_1:70
.=
[(o2 . (pr1 s1)),((o4 | ((arity o4) -tuples_on B3)) . (pr2 s1))]
by A36, UNIALG_2:def 6
.=
[(o2 . (pr1 s1)),(o4 . (pr2 s1))]
by A47, A48, FUNCT_1:70
;
hence
[[:(o2 /. B1),(o4 /. B3):]] . x = ([[:o2,o4:]] | ((arity o24) -tuples_on B)) . x
by A44;
:: thesis: verum end;
thus (Opers [:U2,U4:],B) . n =
o24 /. B
by A24, A25, A30, UNIALG_2:def 7
.=
[[:o2,o4:]] | ((arity o24) -tuples_on B)
by A31, A36, UNIALG_2:def 6
.=
[[:(o2 /. B1),(o4 /. B3):]]
by A38, A39, A40, FUNCT_1:9
.=
the
charact of
[:U1,U3:] . n
by A4, A5, A30, A34, A35, Def4
;
:: thesis: verum
end;
hence
( the charact of [:U1,U3:] = Opers [:U2,U4:],B & B is opers_closed )
by A10, A24, FINSEQ_2:10, UNIALG_2:def 5; :: thesis: verum