let L be 1-sorted ; for A, B, C being AlgebraStr over L st A is Subalgebra of B & B is Subalgebra of C holds
A is Subalgebra of C
let A, B, C be AlgebraStr over L; ( A is Subalgebra of B & B is Subalgebra of C implies A is Subalgebra of C )
assume that
A1:
A is Subalgebra of B
and
A2:
B is Subalgebra of C
; A is Subalgebra of C
A3:
the carrier of A c= the carrier of B
by A1, Def3;
then A4:
[: the carrier of A, the carrier of A:] c= [: the carrier of B, the carrier of B:]
by ZFMISC_1:96;
the carrier of B c= the carrier of C
by A2, Def3;
hence
the carrier of A c= the carrier of C
by A3; POLYALG1:def 3 ( 1. A = 1. C & 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus 1. A =
1. B
by A1, Def3
.=
1. C
by A2, Def3
; ( 0. A = 0. C & the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus 0. A =
0. B
by A1, Def3
.=
0. C
by A2, Def3
; ( the addF of A = the addF of C || the carrier of A & the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus the addF of A =
the addF of B || the carrier of A
by A1, Def3
.=
( the addF of C || the carrier of B) || the carrier of A
by A2, Def3
.=
the addF of C || the carrier of A
by A4, FUNCT_1:51
; ( the multF of A = the multF of C || the carrier of A & the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:] )
thus the multF of A =
the multF of B || the carrier of A
by A1, Def3
.=
( the multF of C || the carrier of B) || the carrier of A
by A2, Def3
.=
the multF of C || the carrier of A
by A4, FUNCT_1:51
; the lmult of A = the lmult of C | [: the carrier of L, the carrier of A:]
A5:
[: the carrier of L, the carrier of A:] c= [: the carrier of L, the carrier of B:]
by A3, ZFMISC_1:96;
thus the lmult of A =
the lmult of B | [: the carrier of L, the carrier of A:]
by A1, Def3
.=
( the lmult of C | [: the carrier of L, the carrier of B:]) | [: the carrier of L, the carrier of A:]
by A2, Def3
.=
the lmult of C | [: the carrier of L, the carrier of A:]
by A5, FUNCT_1:51
; verum