let F be non almost_trivial Field; for x being non trivial Element of F
for o being object st not o in [#] F holds
ExField (x,o) is almost_left_invertible
let x be non trivial Element of F; for o being object st not o in [#] F holds
ExField (x,o) is almost_left_invertible
let v be object ; ( not v in [#] F implies ExField (x,v) is almost_left_invertible )
assume
not v in [#] F
; ExField (x,v) is almost_left_invertible
then A1:
for a being Element of F holds a <> v
;
x <> 0. F
by Def2;
then consider xi being Element of F such that
A2:
xi * x = 1. F
by ALGSTR_0:def 39, ALGSTR_0:def 27;
A3:
[#] (ExField (x,v)) = carr (x,v)
by Def8;
v in {v}
by TARSKI:def 1;
then reconsider u1 = v as Element of carr (x,v) by XBOOLE_0:def 3;
reconsider u = u1 as Element of (ExField (x,v)) by Def8;
now for a being Element of (ExField (x,v)) st a <> 0. (ExField (x,v)) holds
a is left_invertible let a be
Element of
(ExField (x,v));
( a <> 0. (ExField (x,v)) implies b1 is left_invertible )assume A4:
a <> 0. (ExField (x,v))
;
b1 is left_invertible
0. F <> x
by Def2;
then
not
0. F in {x}
by TARSKI:def 1;
then
0. F in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider o =
0. F as
Element of
carr (
x,
v)
by XBOOLE_0:def 3;
per cases
( a = v or a <> v )
;
suppose A5:
a = v
;
b1 is left_invertible then
a in {v}
by TARSKI:def 1;
then reconsider a1 =
a as
Element of
carr (
x,
v)
by XBOOLE_0:def 3;
per cases
( xi = x or xi <> x )
;
suppose A6:
xi = x
;
b1 is left_invertible then A7:
the
multF of
F . (
x,
x)
<> x
by A2, Def2;
u * a =
(multR (x,v)) . (
u1,
a1)
by Def8
.=
multR (
u1,
a1)
by Def7
.=
the
multF of
F . (
xi,
x)
by A7, A6, A5, Def6
.=
1. (ExField (x,v))
by A2, Def8
;
hence
a is
left_invertible
by ALGSTR_0:def 27;
verum end; suppose
xi <> x
;
b1 is left_invertible then
not
xi in {x}
by TARSKI:def 1;
then
xi in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider x1i =
xi as
Element of
carr (
x,
v)
by XBOOLE_0:def 3;
reconsider b =
x1i as
Element of
(ExField (x,v)) by Def8;
A8:
the
multF of
F . (
b,
x)
<> x
by A2, Def2;
b * a =
(multR (x,v)) . (
x1i,
a1)
by Def8
.=
multR (
x1i,
a1)
by Def7
.=
the
multF of
F . (
xi,
x)
by A1, A8, A5, Def6
.=
1. (ExField (x,v))
by A2, Def8
;
hence
a is
left_invertible
by ALGSTR_0:def 27;
verum end; end; suppose A9:
a <> v
;
b1 is left_invertible then
not
a in {v}
by TARSKI:def 1;
then A10:
a in ([#] F) \ {x}
by A3, XBOOLE_0:def 3;
reconsider a1 =
a as
Element of
carr (
x,
v)
by Def8;
reconsider aR =
a as
Element of
[#] F by A10;
aR <> 0. F
by A4, Def8;
then consider aRi being
Element of
F such that A11:
aRi * aR = 1. F
by ALGSTR_0:def 39, ALGSTR_0:def 27;
per cases
( aRi = x or aRi <> x )
;
suppose A12:
aRi = x
;
b1 is left_invertible then A13:
the
multF of
F . (
x,
a)
<> x
by A11, Def2;
u * a =
(multR (x,v)) . (
u1,
a1)
by Def8
.=
multR (
u1,
a1)
by Def7
.=
the
multF of
F . (
aRi,
aR)
by A13, A12, A9, Def6
.=
1. (ExField (x,v))
by A11, Def8
;
hence
a is
left_invertible
by ALGSTR_0:def 27;
verum end; suppose
aRi <> x
;
b1 is left_invertible then
not
aRi in {x}
by TARSKI:def 1;
then
aRi in ([#] F) \ {x}
by XBOOLE_0:def 5;
then reconsider a1i =
aRi as
Element of
carr (
x,
v)
by XBOOLE_0:def 3;
reconsider b =
a1i as
Element of
(ExField (x,v)) by Def8;
A14:
the
multF of
F . (
b,
a)
<> x
by A11, Def2;
A15:
(
aR <> v &
aRi <> v )
by A1;
b * a =
(multR (x,v)) . (
aRi,
a1)
by Def8
.=
multR (
a1i,
a1)
by Def7
.=
the
multF of
F . (
aRi,
aR)
by A15, A14, Def6
.=
1. (ExField (x,v))
by A11, Def8
;
hence
a is
left_invertible
by ALGSTR_0:def 27;
verum end; end; end;
hence
ExField (x,v) is almost_left_invertible
by ALGSTR_0:def 27; verum