let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr of L
for A being Subset of B st A is opers_closed holds
ex C being strict Subalgebra of B st the carrier of C = A
let B be non empty AlgebraStr of L; :: thesis: for A being Subset of B st A is opers_closed holds
ex C being strict Subalgebra of B st the carrier of C = A
let A be Subset of B; :: thesis: ( A is opers_closed implies ex C being strict Subalgebra of B st the carrier of C = A )
assume A1:
A is opers_closed
; :: thesis: ex C being strict Subalgebra of B st the carrier of C = A
A2:
[:A,A:] c= [:the carrier of B,the carrier of B:]
by ZFMISC_1:119;
reconsider f1 = the addF of B || A as Function ;
( dom f1 = [:A,A:] & ( for x being set st x in [:A,A:] holds
f1 . x in A ) )
proof
[:A,A:] c= dom the
addF of
B
by A2, Th1;
hence
dom f1 = [:A,A:]
by RELAT_1:91;
:: thesis: for x being set st x in [:A,A:] holds
f1 . x in A
let x be
set ;
:: thesis: ( x in [:A,A:] implies f1 . x in A )
assume A3:
x in [:A,A:]
;
:: thesis: f1 . x in A
consider y,
z being
set such that A4:
(
y in A &
z in A &
x = [y,z] )
by A3, ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
Element of
B by A4;
A5:
A is
linearly-closed
by A1, Def4;
f1 . x = y + z
by A3, A4, FUNCT_1:72;
hence
f1 . x in A
by A4, A5, VECTSP_4:def 1;
:: thesis: verum
end;
then reconsider ad = f1 as BinOp of A by FUNCT_2:5;
reconsider f2 = the multF of B || A as Function ;
[:A,A:] c= dom the multF of B
by A2, Th1;
then A6:
dom f2 = [:A,A:]
by RELAT_1:91;
for x being set st x in [:A,A:] holds
f2 . x in A
proof
let x be
set ;
:: thesis: ( x in [:A,A:] implies f2 . x in A )
assume A7:
x in [:A,A:]
;
:: thesis: f2 . x in A
consider y,
z being
set such that A8:
(
y in A &
z in A &
x = [y,z] )
by A7, ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
Element of
B by A8;
f2 . x = y * z
by A7, A8, FUNCT_1:72;
hence
f2 . x in A
by A1, A8, Def4;
:: thesis: verum
end;
then reconsider mu = f2 as BinOp of A by A6, FUNCT_2:5;
reconsider f4 = the lmult of B | [:the carrier of L,A:] as Function ;
[:the carrier of L,A:] c= [:the carrier of L,the carrier of B:]
by ZFMISC_1:119;
then
[:the carrier of L,A:] c= dom the lmult of B
by Th2;
then A9:
dom f4 = [:the carrier of L,A:]
by RELAT_1:91;
for x being set st x in [:the carrier of L,A:] holds
f4 . x in A
proof
let x be
set ;
:: thesis: ( x in [:the carrier of L,A:] implies f4 . x in A )
assume A10:
x in [:the carrier of L,A:]
;
:: thesis: f4 . x in A
consider y,
z being
set such that A11:
(
y in the
carrier of
L &
z in A &
x = [y,z] )
by A10, ZFMISC_1:def 2;
reconsider y =
y as
Element of
L by A11;
reconsider z =
z as
Element of
B by A11;
A12:
A is
linearly-closed
by A1, Def4;
f4 . x = y * z
by A10, A11, FUNCT_1:72;
hence
f4 . x in A
by A11, A12, VECTSP_4:def 1;
:: thesis: verum
end;
then reconsider lm = f4 as Function of [:the carrier of L,A:],A by A9, FUNCT_2:5;
reconsider z = 0. B as Element of A by A1, Def4;
reconsider u = 1. B as Element of A by A1, Def4;
set c = AlgebraStr(# A,ad,mu,z,u,lm #);
A13:
1. AlgebraStr(# A,ad,mu,z,u,lm #) = 1. B
;
0. AlgebraStr(# A,ad,mu,z,u,lm #) = 0. B
;
then reconsider C = AlgebraStr(# A,ad,mu,z,u,lm #) as strict Subalgebra of B by A13, Def3;
take
C
; :: thesis: the carrier of C = A
thus
the carrier of C = A
; :: thesis: verum