let K be Field; for F being K -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is associative
let F be K -monomorphic Field; for f being Monomorphism of K,F st K,F are_disjoint holds
embField f is associative
let f be Monomorphism of K,F; ( K,F are_disjoint implies embField f is associative )
assume AS:
K,F are_disjoint
; embField f is associative
now for a, b, c being Element of (embField f) holds a * (b * c) = (a * b) * clet a,
b,
c be
Element of
(embField f);
b1 * (b2 * b3) = (b1 * b2) * b3reconsider x =
a,
y =
b,
z =
c as
Element of
carr f by defemb;
per cases
( a = 0. K or b = 0. K or c = 0. K or ( a <> 0. K & b <> 0. K & c <> 0. K ) )
;
suppose O:
(
a = 0. K or
b = 0. K or
c = 0. K )
;
b1 * (b2 * b3) = (b1 * b2) * b3reconsider bb =
b,
ab =
a * b,
bc =
b * c as
Element of
carr f by defemb;
per cases
( a = 0. K or b = 0. K or c = 0. K )
by O;
suppose A:
a = 0. K
;
b1 * (b2 * b3) = (b1 * b2) * b3A1:
a * b =
(multemb f) . (
x,
bb)
by defemb
.=
multemb (
f,
x,
bb)
by defmult
.=
0. K
by A, defmultf
;
A2:
(a * b) * c =
(multemb f) . (
ab,
z)
by defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
0. K
by A1, defmultf
;
thus a * (b * c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(a * b) * c
by A2, A, defmultf
;
verum end; end; suppose O:
(
a <> 0. K &
b <> 0. K &
c <> 0. K )
;
(b1 * b2) * b3 = b1 * (b2 * b3)per cases
( x in [#] K or not x in [#] K )
;
suppose X:
x in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider a1 =
a as
Element of
K ;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y:
y in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider b1 =
b as
Element of
K ;
X0:
a * b = a1 * b1
by Lm11;
then reconsider ab =
a * b as
Element of
carr f by XBOOLE_0:def 3;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
not
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
F by Lm1;
reconsider bc =
b * c as
Element of
carr f by defemb;
reconsider fa =
f . a1,
fb =
f . b1 as
Element of
F ;
X1:
f . (a1 * b1) = fa * fb
by GROUP_6:def 6;
X2:
b * c = fb * c1
by AS, O, Y, Z, Lm10;
X3:
not
fb * c1 in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) * c =
(multemb f) . (
(a * b),
z)
by defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(fa * fb) * c1
by O, VECTSP_2:def 1, X1, X0, defmultf, Z
.=
fa * (fb * c1)
by GROUP_1:def 3
.=
multemb (
f,
x,
bc)
by O, X3, X2, defmultf
.=
(multemb f) . (
x,
(b * c))
by defmult
.=
a * (b * c)
by defemb
;
verum end; end; suppose Y:
not
y in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider b1 =
b as
Element of
F by Lm1;
reconsider fa =
f . a1 as
Element of
F ;
X0:
a * b = fa * b1
by AS, O, X, Y, Lm10;
then reconsider ab =
fa * b1 as
Element of
carr f by defemb;
X1:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
K ;
reconsider fc =
f . c1 as
Element of
F ;
X2:
b * c = b1 * fc
by AS, O, Y, Z, Lm10;
then reconsider bc =
b1 * fc as
Element of
carr f by defemb;
X3:
not
bc in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) * c =
(fa * b1) * fc
by AS, O, X1, X0, Z, Lm10
.=
fa * (b1 * fc)
by GROUP_1:def 3
.=
a * (b * c)
by AS, O, X, X2, X3, Lm10
;
verum end; suppose Z:
not
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
F by Lm1;
reconsider fa1 =
f . a1 as
Element of
rng f by FUNCT_2:4;
K5: the
multF of
F . (
ab,
z) =
(fa * b1) * c1
.=
fa * (b1 * c1)
by GROUP_1:def 3
;
per cases
( the multF of F . (ab,z) in rng f or not the multF of F . (ab,z) in rng f )
;
suppose K:
the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X2:
(a * b) * c =
(multemb f) . (
ab,
z)
by X0, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(f ") . ((fa * b1) * c1)
by X1, Z, defmultf, K
.=
(f ") . (fa * (b1 * c1))
by GROUP_1:def 3
;
K1:
now the multF of F . (y,z) in rng fassume K7:
not the
multF of
F . (
y,
z)
in rng f
;
contradictionX4:
not the
multF of
F . (
b1,
c1)
in [#] K
by AS, XBOOLE_0:def 4;
X3:
b * c = b1 * c1
by AS, Y, Z, Lm12, K7;
b1 * c1 in ([#] F) \ (rng f)
by K7, XBOOLE_0:def 5;
then reconsider bc1 =
b1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
reconsider bce =
bc1 as
Element of
(embField f) by X3;
the
multF of
F . (
(f . a),
bce)
in ([#] F) \ (rng f)
by O, X, X4, Lm5;
hence
contradiction
by K5, K, XBOOLE_0:def 5;
verum end; then X3:
b * c = (f ") . (b1 * c1)
by Y, Z, Lm13;
(f ") . (b1 * c1) in [#] K
by K1, FUNCT_2:5;
then reconsider bc =
(f ") . (b1 * c1) as
Element of
carr f by XBOOLE_0:def 3;
reconsider bc1 =
b1 * c1 as
Element of
rng f by K1;
thus (a * b) * c =
((f ") . fa1) * ((f ") . bc1)
by Th1, X2
.=
a1 * ((f ") . bc1)
by FUNCT_2:26
.=
multemb (
f,
x,
bc)
by defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X3, defemb
;
verum end; suppose K:
not the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X4:
ab <> 0. K
by AS, XBOOLE_0:def 4;
X2:
(a * b) * c =
(multemb f) . (
ab,
z)
by X0, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(fa * b1) * c1
by O, X4, X1, Z, defmultf, K
.=
fa * (b1 * c1)
by GROUP_1:def 3
;
then
b1 * c1 in ([#] F) \ (rng f)
by XBOOLE_0:def 5;
then reconsider bc =
b1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
X3:
b * c = b1 * c1
by AS, K1, Y, Z, Lm12;
not
b1 * c1 in [#] K
by AS, XBOOLE_0:def 4;
hence (a * b) * c =
multemb (
f,
x,
bc)
by O, X2, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X3, defemb
;
verum end; end; end; end; suppose X:
not
x in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider a1 =
a as
Element of
F by Lm1;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y:
y in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider b1 =
b as
Element of
K ;
X0:
a * b = a1 * (f . b1)
by AS, O, X, Y, Lm10;
reconsider ab =
a * b as
Element of
carr f by defemb;
reconsider fb =
f . b1 as
Element of
F ;
X2:
not
ab in [#] K
by AS, O, X, Y, Lm10;
per cases
( z in [#] K or not z in [#] K )
;
suppose
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
K ;
reconsider fc =
f . c1 as
Element of
F ;
X3:
b * c = b1 * c1
by Lm11;
then reconsider bc =
b * c as
Element of
carr f by XBOOLE_0:def 3;
thus (a * b) * c =
(multemb f) . (
ab,
z)
by defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(a1 * fb) * fc
by O, X0, X2, defmultf
.=
a1 * (fb * fc)
by GROUP_1:def 3
.=
a1 * (f . (b1 * c1))
by GROUP_6:def 6
.=
multemb (
f,
x,
bc)
by defmultf, X3, X, O, VECTSP_2:def 1
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by defemb
;
verum end; suppose Z:
not
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
F by Lm1;
X3:
b * c = (f . b1) * c1
by AS, O, Y, Z, Lm10;
reconsider bc =
b * c as
Element of
carr f by defemb;
X5:
not
b * c in [#] K
by AS, O, Y, Z, Lm10;
K5: the
multF of
F . (
ab,
z) =
(a1 * fb) * c1
by AS, O, X, Y, Lm10
.=
a1 * (fb * c1)
by GROUP_1:def 3
.=
the
multF of
F . (
x,
bc)
by AS, O, Y, Z, Lm10
;
per cases
( not the multF of F . (ab,z) in rng f or the multF of F . (ab,z) in rng f )
;
suppose K:
not the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)hence (a * b) * c =
(a1 * fb) * c1
by AS, X0, X2, Z, Lm12
.=
a1 * (fb * c1)
by GROUP_1:def 3
.=
a * (b * c)
by AS, K, K5, X3, X, X5, Lm12
;
verum end; suppose K:
the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)thus (a * b) * c =
(multemb f) . (
ab,
z)
by defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(f ") . ( the multF of F . (ab,z))
by K, X2, Z, defmultf
.=
multemb (
f,
x,
bc)
by K, K5, X, X5, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by defemb
;
verum end; end; end; suppose Y:
not
y in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider b1 =
b as
Element of
F by Lm1;
per cases
( not the multF of F . (x,y) in rng f or the multF of F . (x,y) in rng f )
;
suppose K:
not the
multF of
F . (
x,
y)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)then X0:
a * b = a1 * b1
by AS, Y, X, Lm12;
a1 * b1 in ([#] F) \ (rng f)
by K, XBOOLE_0:def 5;
then reconsider ab =
a1 * b1 as
Element of
carr f by XBOOLE_0:def 3;
D:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
K ;
X1:
b * c = b1 * (f . c1)
by AS, O, Y, Z, Lm10;
[#] (embField f) = carr f
by defemb;
then X3:
b1 * (f . c1) in ([#] F) \ (rng f)
by O, Y, Lm4;
X2:
not
b1 * (f . c1) in [#] K
by AS, XBOOLE_0:def 4;
reconsider bc =
b1 * (f . c1) as
Element of
carr f by X3, XBOOLE_0:def 3;
X4:
(a * b) * c =
(a1 * b1) * (f . c1)
by AS, O, X0, Z, D, Lm10
.=
a1 * (b1 * (f . c1))
by GROUP_1:def 3
;
X5: the
multF of
F . (
x,
bc) =
a1 * (b1 * (f . c1))
.=
(a1 * b1) * (f . c1)
by GROUP_1:def 3
.=
the
multF of
F . (
ab,
(f . z))
;
the
multF of
F . (
ab,
(f . z))
in ([#] F) \ (rng f)
by O, D, Lm4, Z;
then H:
not the
multF of
F . (
x,
bc)
in rng f
by X5, XBOOLE_0:def 5;
bc <> 0. K
by AS, XBOOLE_0:def 4;
hence (a * b) * c =
multemb (
f,
x,
bc)
by O, H, X, X2, X4, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X1, defemb
;
verum end; suppose Z:
not
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
F by Lm1;
K5: the
multF of
F . (
ab,
z) =
(a1 * b1) * c1
.=
a1 * (b1 * c1)
by GROUP_1:def 3
.=
the
multF of
F . (
a1,
(b1 * c1))
;
per cases
( not the multF of F . (ab,z) in rng f or the multF of F . (ab,z) in rng f )
;
suppose K:
not the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)per cases
( not the multF of F . (b1,c1) in rng f or the multF of F . (b1,c1) in rng f )
;
suppose K6:
not the
multF of
F . (
b1,
c1)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X1:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
b1 * c1
by O, defmultf, Y, Z, K6
;
K9:
the
multF of
F . (
b1,
c1)
in ([#] F) \ (rng f)
by K6, XBOOLE_0:def 5;
K8:
not
b1 * c1 in [#] K
by AS, XBOOLE_0:def 4;
reconsider bc =
b1 * c1 as
Element of
carr f by K9, XBOOLE_0:def 3;
X4:
(
ab <> 0. K &
bc <> 0. K )
by AS, XBOOLE_0:def 4;
thus (a * b) * c =
(multemb f) . (
ab,
z)
by X0, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(a1 * b1) * c1
by X4, O, D, Z, defmultf, K
.=
multemb (
f,
x,
bc)
by X4, O, X, K5, K, K8, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X1, defemb
;
verum end; suppose K6:
the
multF of
F . (
b1,
c1)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X1:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
(f ") . (b1 * c1)
by defmultf, Y, Z, K6
;
b1 * c1 in dom (f ")
by K6, FUNCT_1:33;
then
(f ") . (b1 * c1) in rng (f ")
by FUNCT_1:3;
then reconsider bc1 =
(f ") . (b1 * c1) as
Element of
[#] K ;
reconsider bc =
bc1 as
Element of
carr f by XBOOLE_0:def 3;
M0:
dom f = [#] K
by FUNCT_2:def 1;
f . (0. K) = 0. F
by RING_2:6;
then M1:
0. F in rng f
by M0, FUNCT_1:def 3;
then M2:
c1 <> 0. F
by Z, Lm1;
b1 <> 0. F
by M1, Y, Lm1;
then
b1 * c1 <> 0. F
by M2, VECTSP_2:def 1;
then X4:
(
bc <> 0. K &
ab <> 0. K )
by AS, XBOOLE_0:def 4, K6, Th2;
thus (a * b) * c =
(multemb f) . (
ab,
z)
by X0, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(a1 * b1) * c1
by X4, O, D, Z, defmultf, K
.=
a1 * (b1 * c1)
by GROUP_1:def 3
.=
a1 * (f . bc1)
by K6, FUNCT_1:35
.=
multemb (
f,
x,
bc)
by X4, X, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X1, defemb
;
verum end; suppose K7:
the
multF of
F . (
ab,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)K6:
now not the multF of F . (b1,c1) in rng fassume
the
multF of
F . (
b1,
c1)
in rng f
;
contradictionthen consider x being
object such that H1:
(
x in dom f &
f . x = b1 * c1 )
by FUNCT_1:def 3;
consider y being
object such that H2:
(
y in dom f &
f . y = (a1 * b1) * c1 )
by K7, FUNCT_1:def 3;
reconsider xx =
x,
yy =
y as
Element of
K by H1, H2;
B3h:
dom f = [#] K
by FUNCT_2:def 1;
B3a:
(
a in [#] F & not
a in rng f )
by X, Lm1;
f . (0. K) = 0. F
by RING_2:6;
then
0. F in rng f
by B3h, FUNCT_1:def 3;
then OO:
(
a1 <> 0. F &
b1 <> 0. F &
c1 <> 0. F )
by X, Y, Z, Lm1;
then
xx <> 0. K
by H1, RING_2:6, VECTSP_2:def 1;
then f . (xx ") =
(b1 * c1) "
by Th5, H1
.=
(c1 ") * (b1 ")
by OO, VECTSP_2:11
.=
(b1 ") * (c1 ")
by GROUP_1:def 12
;
then (f . yy) * (f . (xx ")) =
(a1 * (b1 * c1)) * ((b1 ") * (c1 "))
by H2, GROUP_1:def 3
.=
a1 * ((b1 * c1) * ((b1 ") * (c1 ")))
by GROUP_1:def 3
.=
a1 * (b1 * (c1 * ((b1 ") * (c1 "))))
by GROUP_1:def 3
.=
a1 * (b1 * (c1 * ((c1 ") * (b1 "))))
by GROUP_1:def 12
.=
a1 * (b1 * ((c1 * (c1 ")) * (b1 ")))
by GROUP_1:def 3
.=
a1 * (b1 * (((c1 ") * c1) * (b1 ")))
by GROUP_1:def 12
.=
a1 * (b1 * ((1. F) * (b1 ")))
by OO, VECTSP_1:def 10
.=
a1 * ((b1 ") * b1)
by GROUP_1:def 12
.=
a1 * (1. F)
by OO, VECTSP_1:def 10
;
then B4:
a1 = f . (yy * (xx "))
by GROUP_6:def 6;
dom f = [#] K
by FUNCT_2:def 1;
hence
contradiction
by B3a, B4, FUNCT_1:def 3;
verum end; X1:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
b1 * c1
by O, defmultf, Y, Z, K6
;
b1 * c1 in ([#] F) \ (rng f)
by K6, XBOOLE_0:def 5;
then reconsider bc =
b1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
K9:
not
bc in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) * c =
(multemb f) . (
ab,
z)
by X0, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(f ") . ((a1 * b1) * c1)
by D, Z, defmultf, K7
.=
multemb (
f,
x,
bc)
by X, K5, K7, defmultf, K9
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X1, defemb
;
verum end; end; suppose L:
the
multF of
F . (
x,
y)
in rng f
;
b1 * (b2 * b3) = (b1 * b2) * b3Z1:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by defmultf, X, Y, L
;
a1 * b1 in dom (f ")
by L, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
[#] K ;
reconsider ab =
ab1 as
Element of
carr f by XBOOLE_0:def 3;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
b1 * (b2 * b3) = (b1 * b2) * b3then reconsider c1 =
c as
Element of
K ;
Z2:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
b1 * (f . c1)
by O, defmultf, Y
;
then L0:
b * c in ([#] F) \ (rng f)
by O, Lm4, Y, Z;
reconsider bc1 =
b1 * (f . c1) as
Element of
F ;
reconsider bc =
bc1 as
Element of
carr f by Z2, L0, XBOOLE_0:def 3;
Z3:
(a * b) * c =
(multemb f) . (
ab,
z)
by Z1, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
ab1 * c1
by defmultf
;
Z4:
not
bc in [#] K
by AS, XBOOLE_0:def 4;
Z9:
(
dom f = [#] K &
rng f c= [#] F )
by FUNCT_2:def 1;
L2:
dom f = [#] K
by FUNCT_2:def 1;
then reconsider fc1 =
f . c1 as
Element of
rng f by FUNCT_1:def 3;
reconsider ffc1 =
(f ") . fc1 as
Element of
K ;
(f ") . fc1 = c1
by L2, FUNCT_1:34;
then Z5:
(f ") . ((a1 * b1) * fc1) = ab1 * c1
by L, Th1;
consider x1 being
object such that Z6:
(
x1 in dom f &
f . x1 = a1 * b1 )
by L, FUNCT_1:def 3;
reconsider xx =
x1 as
Element of
K by Z6;
f . (xx * c1) = (a1 * b1) * (f . c1)
by Z6, GROUP_6:def 6;
then
(a1 * b1) * (f . c1) in rng f
by Z9, FUNCT_1:def 3;
then L1:
a1 * (b1 * (f . c1)) in rng f
by GROUP_1:def 3;
thus a * (b * c) =
(multemb f) . (
x,
bc)
by Z2, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f ") . (a1 * bc1)
by L1, Z4, X, defmultf
.=
(a * b) * c
by Z3, Z5, GROUP_1:def 3
;
verum end; suppose Z:
not
z in [#] K
;
(b1 * b2) * b3 = b1 * (b2 * b3)then reconsider c1 =
c as
Element of
F by Lm1;
M0:
dom f = [#] K
by FUNCT_2:def 1;
f . (0. K) = 0. F
by RING_2:6;
then M1:
0. F in rng f
by M0, FUNCT_1:def 3;
then M2:
a1 <> 0. F
by X, Lm1;
b1 <> 0. F
by M1, Y, Lm1;
then
a1 * b1 <> 0. F
by M2, VECTSP_2:def 1;
then Z0:
ab <> 0. K
by L, Th2;
Z2:
(a * b) * c =
(multemb f) . (
ab,
z)
by Z1, defemb
.=
multemb (
f,
ab,
z)
by defmult
.=
(f . ab1) * c1
by Z, Z0, defmultf
.=
(a1 * b1) * c1
by L, FUNCT_1:35
.=
a1 * (b1 * c1)
by GROUP_1:def 3
;
f . ((f ") . (a1 * b1)) = a1 * b1
by FUNCT_1:35, L;
then
(a1 * b1) * c1 in ([#] F) \ (rng f)
by Z0, Z, Lm5;
then
a1 * (b1 * c1) in ([#] F) \ (rng f)
by GROUP_1:def 3;
then U2:
not the
multF of
F . (
a,
(b1 * c1))
in rng f
by XBOOLE_0:def 5;
per cases
( not the multF of F . (y,z) in rng f or the multF of F . (y,z) in rng f )
;
suppose L1:
not the
multF of
F . (
y,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X3:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
b1 * c1
by O, L1, Y, Z, defmultf
;
X4:
b1 * c1 in ([#] F) \ (rng f)
by L1, XBOOLE_0:def 5;
reconsider bc1 =
b1 * c1 as
Element of
F ;
reconsider bc =
bc1 as
Element of
carr f by X4, XBOOLE_0:def 3;
( not
bc in [#] K &
bc <> 0. K )
by AS, XBOOLE_0:def 4;
hence (a * b) * c =
multemb (
f,
x,
bc)
by O, Z2, U2, X, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X3, defemb
;
verum end; suppose K6:
the
multF of
F . (
y,
z)
in rng f
;
(b1 * b2) * b3 = b1 * (b2 * b3)X1:
b * c =
(multemb f) . (
y,
z)
by defemb
.=
multemb (
f,
y,
z)
by defmult
.=
(f ") . (b1 * c1)
by defmultf, Y, Z, K6
;
b1 * c1 in dom (f ")
by K6, FUNCT_1:33;
then
(f ") . (b1 * c1) in rng (f ")
by FUNCT_1:3;
then reconsider bc1 =
(f ") . (b1 * c1) as
Element of
[#] K ;
reconsider bc =
bc1 as
Element of
carr f by XBOOLE_0:def 3;
M0:
dom f = [#] K
by FUNCT_2:def 1;
f . (0. K) = 0. F
by RING_2:6;
then M1:
0. F in rng f
by M0, FUNCT_1:def 3;
then M2:
c1 <> 0. F
by Z, Lm1;
b1 <> 0. F
by M1, Y, Lm1;
then
b1 * c1 <> 0. F
by M2, VECTSP_2:def 1;
then X2:
bc <> 0. K
by K6, Th2;
thus (a * b) * c =
a1 * (f . bc1)
by Z2, K6, FUNCT_1:35
.=
multemb (
f,
x,
bc)
by X2, X, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b * c)
by X1, defemb
;
verum end; end; end; end; end; end;
hence
embField f is associative
; verum