set C1 = [#] K;
A1:
( the addF of K = the addF of K || ([#] K) & the multF of K = the multF of K || ([#] K) )
by RELSET_1:19;
set ST = doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #);
( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is right_complementable & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )
proof
thus
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) is
right_complementable
( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is commutative & doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )proof
let x be
Element of
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #);
ALGSTR_0:def 16 x is right_complementable
reconsider x1 =
x as
Element of
K ;
consider v being
Element of
K such that A2:
x1 + v = 0. K
by ALGSTR_0:def 11;
reconsider y =
v as
Element of
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) ;
take
y
;
ALGSTR_0:def 11 x + y = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus
x + y = 0. doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #)
by A2;
verum
end;
thus
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) is
commutative
( doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is almost_left_invertible & not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated )
thus
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) is
almost_left_invertible
not doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is degenerated proof
let x be
Element of
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #);
VECTSP_1:def 9 ( x = 0. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) or ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) )
assume A3:
x <> 0. doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #)
;
ex b1 being Element of the carrier of doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) st b1 * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
reconsider x1 =
x as
Element of
K ;
x1 is
left_invertible
by A3, ALGSTR_0:def 39;
then consider v being
Element of
K such that A4:
v * x1 = 1. K
;
reconsider y =
v as
Element of
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) ;
take
y
;
y * x = 1. doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #)
thus
y * x = 1. doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #)
by A4;
verum
end;
thus
not
doubleLoopStr(# the
carrier of
K, the
addF of
K, the
multF of
K,
(1. K),
(0. K) #) is
degenerated
;
verum
end;
then
doubleLoopStr(# the carrier of K, the addF of K, the multF of K,(1. K),(0. K) #) is Subfield of K
by A1, Th2;
hence
ex b1 being Subfield of K st b1 is strict
; verum