let K be Field; for ST being non empty doubleLoopStr st the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated holds
ST is Subfield of K
let ST be non empty doubleLoopStr ; ( the carrier of ST is Subset of the carrier of K & the addF of ST = the addF of K || the carrier of ST & the multF of ST = the multF of K || the carrier of ST & 1. ST = 1. K & 0. ST = 0. K & ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated implies ST is Subfield of K )
assume that
A1:
the carrier of ST is Subset of the carrier of K
and
A2:
the addF of ST = the addF of K || the carrier of ST
and
A3:
the multF of ST = the multF of K || the carrier of ST
and
A4:
1. ST = 1. K
and
A5:
0. ST = 0. K
and
A6:
( ST is right_complementable & ST is commutative & ST is almost_left_invertible & not ST is degenerated )
; ST is Subfield of K
set C1 = the carrier of ST;
set AC = the addF of ST;
set MC = the multF of ST;
set d0 = 0. ST;
set d1 = 1. ST;
( ST is Abelian & ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
proof
set MK = the
multF of
K;
set AK = the
addF of
K;
hereby VECTSP_1:def 7 verum
let a,
x,
y be
Element of
ST;
( a * (x + y) = (a * x) + (a * y) & (x + y) * a = (x * a) + (y * a) )reconsider x1 =
x,
y1 =
y,
a1 =
a as
Element of
K by A1, TARSKI:def 3;
(x + y) * a = the
multF of
K . (
(x + y),
a)
by A7;
then
(x + y) * a = (x1 + y1) * a1
by A8;
then
(x + y) * a = (x1 * a1) + (y1 * a1)
by VECTSP_1:def 7;
then
(x + y) * a = the
addF of
K . (
( the multF of K . (x1,a1)),
(y * a))
by A7;
then A11:
(x + y) * a = the
addF of
K . (
(x * a),
(y * a))
by A7;
a * (x + y) = the
multF of
K . (
a,
(x + y))
by A7;
then
a * (x + y) = a1 * (x1 + y1)
by A8;
then
a * (x + y) = (a1 * x1) + (a1 * y1)
by VECTSP_1:def 7;
then
a * (x + y) = the
addF of
K . (
( the multF of K . (a,x1)),
(a * y))
by A7;
then
a * (x + y) = the
addF of
K . (
(a * x),
(a * y))
by A7;
hence
(
a * (x + y) = (a * x) + (a * y) &
(x + y) * a = (x * a) + (y * a) )
by A8, A11;
verum
end;
end;
hence
ST is Subfield of K
by A1, A2, A3, A4, A5, A6, Def1; verum