thus
embField f is commutative
embField f is well-unital proof
now for a, b being Element of (embField f) holds a * b = b * alet a,
b be
Element of
(embField f);
b1 * b2 = b2 * b1reconsider x =
a,
y =
b as
Element of
carr f by defemb;
per cases
( ( x in [#] K & y in [#] K ) or a = 0. K or b = 0. K or ( x in [#] K & x <> 0. K & not y in [#] K ) or ( y in [#] K & y <> 0. K & not x in [#] K ) or ( not x in [#] K & not y in [#] K & the multF of T . (x,y) in rng f ) or ( not x in [#] K & not y in [#] K & not the multF of T . (x,y) in rng f ) )
;
suppose A:
( not
x in [#] K & not
y in [#] K & the
multF of
T . (
x,
y)
in rng f )
;
b1 * b2 = b2 * b1then reconsider a1 =
a,
b1 =
b as
Element of
T by Lm1;
B: the
multF of
T . (
a,
b) =
a1 * b1
.=
b1 * a1
by GROUP_1:def 12
.=
the
multF of
T . (
b,
a)
;
thus a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by A, defmultf
.=
multemb (
f,
y,
x)
by A, B, defmultf
.=
(multemb f) . (
y,
x)
by defmult
.=
b * a
by defemb
;
verum end; suppose A:
( not
x in [#] K & not
y in [#] K & not the
multF of
T . (
x,
y)
in rng f )
;
b1 * b2 = b2 * b1then reconsider a1 =
a,
b1 =
b as
Element of
T by Lm1;
C:
(
a <> 0. K &
b <> 0. K )
by A;
B: the
multF of
T . (
a,
b) =
a1 * b1
.=
b1 * a1
by GROUP_1:def 12
.=
the
multF of
T . (
b,
a)
;
thus a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
the
multF of
T . (
a,
b)
by C, A, defmultf
.=
multemb (
f,
y,
x)
by C, A, B, defmultf
.=
(multemb f) . (
y,
x)
by defmult
.=
b * a
by defemb
;
verum end; end;
hence
embField f is
commutative
;
verum
end;
thus
embField f is well-unital
verumproof
now for a being Element of (embField f) holds
( a * (1. (embField f)) = a & (1. (embField f)) * a = a )let a be
Element of
(embField f);
( b1 * (1. (embField f)) = b1 & (1. (embField f)) * b1 = b1 )reconsider x =
a as
Element of
carr f by defemb;
reconsider e =
1. (embField f) as
Element of
carr f by defemb;
B:
a * (1. (embField f)) =
(multemb f) . (
x,
e)
by defemb
.=
multemb (
f,
x,
e)
by defmult
;
D:
(1. (embField f)) * a =
(multemb f) . (
e,
x)
by defemb
.=
multemb (
f,
e,
x)
by defmult
;
C:
1. (embField f) = 1. K
by defemb;
per cases
( x in [#] K or not x in [#] K )
;
suppose A:
not
x in [#] K
;
( b1 * (1. (embField f)) = b1 & (1. (embField f)) * b1 = b1 )then reconsider a1 =
a as
Element of
T by Lm1;
E:
(
e in [#] K &
e <> 0. K )
by C;
then multemb (
f,
x,
e) =
the
multF of
T . (
a1,
(f . e))
by A, defmultf
.=
the
multF of
T . (
a1,
(f . (1_ K)))
by defemb
.=
a1 * (1_ T)
by GROUP_1:def 13
;
hence
a * (1. (embField f)) = a
by B;
(1. (embField f)) * a = a multemb (
f,
e,
x) =
the
multF of
T . (
(f . e),
a1)
by E, A, defmultf
.=
the
multF of
T . (
(f . (1_ K)),
a1)
by defemb
.=
(1_ T) * a1
by GROUP_1:def 13
;
hence
(1. (embField f)) * a = a
by D;
verum end; end;
hence
embField f is
well-unital
;
verum
end;