let K be Field; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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;
A7: now :: thesis: for a, x being Element of ST holds a * x = the multF of K . (a,x)
let a, x be Element of ST; :: thesis: a * x = the multF of K . (a,x)
a * x = the multF of K . [a,x] by A3, FUNCT_1:49;
hence a * x = the multF of K . (a,x) ; :: thesis: verum
end;
A8: now :: thesis: for x, y being Element of ST holds x + y = the addF of K . (x,y)
let x, y be Element of ST; :: thesis: x + y = the addF of K . (x,y)
x + y = the addF of K . [x,y] by A2, FUNCT_1:49;
hence x + y = the addF of K . (x,y) ; :: thesis: verum
end;
( 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 :: according to RLVECT_1:def 2 :: thesis: ( ST is add-associative & ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
let x, y be Element of ST; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as Element of K by A1, TARSKI:def 3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 3 :: thesis: ( ST is right_zeroed & ST is associative & ST is well-unital & ST is distributive )
let x, y, z be Element of ST; :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as Element of K by A1, TARSKI:def 3;
x + (y + z) = the addF of K . (x1,(y + z)) by A8;
then A9: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of K . ((x + y),z1) by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A9, RLVECT_1:def 3; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 4 :: thesis: ( ST is associative & ST is well-unital & ST is distributive )
let x be Element of ST; :: thesis: x + (0. ST) = x
reconsider y = x, z = 0. ST as Element of K by A1, TARSKI:def 3;
x + (0. ST) = y + (0. K) by A5, A8;
hence x + (0. ST) = x by RLVECT_1:4; :: thesis: verum
end;
hereby :: according to GROUP_1:def 3 :: thesis: ( ST is well-unital & ST is distributive )
let a, b, x be Element of ST; :: thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of K by A1, TARSKI:def 3;
a * (b * x) = the multF of K . (a,(b * x)) by A7;
then A10: a * (b * x) = a1 * (b1 * y) by A7;
a * b = a1 * b1 by A7;
then (a * b) * x = (a1 * b1) * y by A7;
hence (a * b) * x = a * (b * x) by A10, GROUP_1:def 3; :: thesis: verum
end;
hereby :: according to VECTSP_1:def 6 :: thesis: ST is distributive
let x be Element of ST; :: thesis: ( x * (1. ST) = x & (1. ST) * x = x )
reconsider y = x as Element of K by A1, TARSKI:def 3;
( x * (1. ST) = y * (1. K) & (1. ST) * x = (1. K) * y ) by A4, A7;
hence ( x * (1. ST) = x & (1. ST) * x = x ) ; :: thesis: verum
end;
hereby :: according to VECTSP_1:def 7 :: thesis: verum
let a, x, y be Element of ST; :: thesis: ( 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; :: thesis: verum
end;
end;
hence ST is Subfield of K by A1, A2, A3, A4, A5, A6, Def1; :: thesis: verum