let K be Field; for T being K -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive
let T be K -monomorphic comRing; for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is distributive
let f be Monomorphism of K,T; ( K,T are_disjoint implies embField f is distributive )
assume AS:
K,T are_disjoint
; embField f is distributive
now for a, b, c being Element of (embField f) holds
( a * (b + c) = (a * b) + (a * c) & (b + c) * a = (b * a) + (c * a) )let a,
b,
c be
Element of
(embField f);
( b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) & (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) )reconsider x =
a,
y =
b,
z =
c as
Element of
carr f by defemb;
per cases
( a = 0. K or a <> 0. K )
;
suppose A:
a = 0. K
;
( b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) & (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) )A1:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
0. K
by A, defmultf
;
A2:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
0. K
by A, defmultf
;
reconsider bc =
b + c as
Element of
carr f by defemb;
thus I:
a * (b + c) =
(multemb f) . (
x,
(b + c))
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
0. K
by A, defmultf
.=
0. (embField f)
by defemb
.=
(0. (embField f)) + (0. (embField f))
by RLVECT_1:def 4
.=
(a * b) + (0. (embField f))
by A1, defemb
.=
(a * b) + (a * c)
by A2, defemb
;
(b + c) * a = (b * a) + (c * a)thus (b + c) * a =
a * (b + c)
by GROUP_1:def 12
.=
(b * a) + (a * c)
by I, GROUP_1:def 12
.=
(b * a) + (c * a)
by GROUP_1:def 12
;
verum end; suppose A:
a <> 0. K
;
( b1 * (b2 + b3) = (b1 * b2) + (b1 * b3) & (b2 + b3) * b1 = (b2 * b1) + (b3 * b1) )thus I:
a * (b + c) = (a * b) + (a * c)
(b + c) * a = (b * a) + (c * a)proof
per cases
( b = 0. K or c = 0. K or ( b <> 0. K & c <> 0. K ) )
;
suppose BC:
(
b <> 0. K &
c <> 0. K )
;
a * (b + c) = (a * b) + (a * c)per cases
( x in [#] K or not x in [#] K )
;
suppose X:
x in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider a1 =
a as
Element of
K ;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y:
y in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider b1 =
b as
Element of
K ;
A1:
a * b = a1 * b1
by Lm11;
reconsider ab =
a * b as
Element of
carr f by defemb;
per cases
( c in [#] K or not z in [#] K )
;
suppose Z:
not
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
T by Lm1;
A2:
a * c = (f . a1) * c1
by AS, X, Z, A, Lm10;
A3:
b + c = (f . b1) + c1
by AS, Y, Z, Lm6;
then reconsider bc =
(f . b1) + c1 as
Element of
carr f by defemb;
reconsider ac =
(f . a1) * c1 as
Element of
carr f by A2, defemb;
A4:
not
bc in [#] K
by AS, A3, Y, Z, Lm6;
A5:
not
ac in [#] K
by A2, AS, A, X, Z, Lm10;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by A3, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f . a1) * ((f . b1) + c1)
by A, A4, defmultf
.=
((f . a1) * (f . b1)) + ((f . a1) * c1)
by VECTSP_1:def 7
.=
(f . (a1 * b1)) + ((f . a1) * c1)
by GROUP_6:def 6
.=
addemb (
f,
ab,
ac)
by A5, A1, defaddf
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A2, defemb
;
verum end; end; suppose Y:
not
y in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider b1 =
b as
Element of
T by Lm1;
A1:
a * b = (f . a1) * b1
by AS, X, Y, A, Lm10;
then reconsider ab =
(f . a1) * b1 as
Element of
carr f by defemb;
A5:
not
ab in [#] K
by A1, AS, X, Y, A, Lm10;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
K ;
A2:
a * c = a1 * c1
by Lm11;
A3:
b + c = b1 + (f . c1)
by AS, Y, Z, Lm6;
reconsider bc =
b + c,
ac =
a * c as
Element of
carr f by defemb;
A4:
not
bc in [#] K
by AS, Y, Z, Lm6;
reconsider fc1 =
f . c1 as
Element of
T ;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f . a1) * (b1 + (f . c1))
by A, A3, A4, defmultf
.=
((f . a1) * b1) + ((f . a1) * (f . c1))
by VECTSP_1:def 7
.=
((f . a1) * b1) + (f . (a1 * c1))
by GROUP_6:def 6
.=
addemb (
f,
ab,
ac)
by A5, A2, defaddf
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A1, defemb
;
verum end; suppose Z:
not
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
T by Lm1;
A2:
a * c = (f . a1) * c1
by AS, X, Z, A, Lm10;
reconsider ac =
a * c as
Element of
carr f by defemb;
A6:
not
ac in [#] K
by AS, X, Z, A, Lm10;
per cases
( not the addF of T . (y,z) in rng f or the addF of T . (y,z) in rng f )
;
suppose Z1:
not the
addF of
T . (
y,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)then A3:
b + c = b1 + c1
by AS, Y, Z, Lm8;
reconsider bc =
b + c as
Element of
carr f by defemb;
A4:
not
bc in [#] K
by AS, A3, XBOOLE_0:def 4;
then A8:
the
multF of
T . (
(f . x),
bc)
in ([#] T) \ (rng f)
by A, X, Lm5;
the
multF of
T . (
(f . x),
bc) =
(f . a1) * (b1 + c1)
by Z1, AS, Y, Z, Lm8
.=
((f . a1) * b1) + ((f . a1) * c1)
by VECTSP_1:def 7
.=
the
addF of
T . (
ab,
ac)
by AS, X, Z, A, Lm10
;
then A7:
not the
addF of
T . (
ab,
ac)
in rng f
by A8, XBOOLE_0:def 5;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f . a1) * (b1 + c1)
by A, A3, A4, defmultf
.=
((f . a1) * b1) + ((f . a1) * c1)
by VECTSP_1:def 7
.=
addemb (
f,
ab,
ac)
by A2, A5, A6, A7, defaddf
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A1, defemb
;
verum end; suppose Z1:
the
addF of
T . (
y,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)then A3:
b + c = (f ") . (b1 + c1)
by Y, Z, Lm9;
reconsider bc =
b + c,
ac =
a * c as
Element of
carr f by defemb;
A0:
dom f = [#] K
by FUNCT_2:def 1;
b1 + c1 in dom (f ")
by Z1, FUNCT_1:33;
then
b + c in rng (f ")
by A3, FUNCT_1:3;
then reconsider bc1 =
b + c as
Element of
K ;
A9:
f . (a1 * bc1) =
(f . a1) * (f . bc1)
by GROUP_6:def 6
.=
(f . a1) * (b1 + c1)
by Z1, A3, FUNCT_1:35
.=
((f . a1) * b1) + ((f . a1) * c1)
by VECTSP_1:def 7
;
then A4:
the
addF of
T . (
ab,
ac)
in rng f
by A0, A2, FUNCT_1:def 3;
reconsider fa1 =
f . a1 as
Element of
rng f by A0, FUNCT_1:3;
reconsider fbc1 =
f . bc1 as
Element of
rng f by A0, FUNCT_1:3;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * bc1
by defmultf
.=
(f ") . (((f . a1) * b1) + ((f . a1) * c1))
by A9, A0, FUNCT_1:34
.=
addemb (
f,
ab,
ac)
by A2, A4, A5, A6, defaddf
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A1, defemb
;
verum end; end; end; end; suppose X:
not
x in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider a1 =
a as
Element of
T by Lm1;
B0:
dom f = [#] K
by FUNCT_2:def 1;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y:
y in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider b1 =
b as
Element of
K ;
A1:
a * b = a1 * (f . b1)
by AS, X, Y, BC, Lm10;
then reconsider ab =
a1 * (f . b1) as
Element of
carr f by defemb;
A2:
not
ab in [#] K
by A1, AS, X, Y, BC, Lm10;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
K ;
A3:
a * c = a1 * (f . c1)
by AS, X, Z, BC, Lm10;
then reconsider ac =
a1 * (f . c1) as
Element of
carr f by defemb;
A4:
not
ac in [#] K
by A3, AS, X, Z, BC, Lm10;
A5:
b + c =
(addemb f) . (
y,
z)
by defemb
.=
addemb (
f,
y,
z)
by defadd
.=
b1 + c1
by defaddf
;
then reconsider bc1 =
b + c as
Element of
K ;
reconsider bc =
b + c as
Element of
carr f by defemb;
per cases
( bc = 0. K or bc <> 0. K )
;
suppose O:
bc = 0. K
;
a * (b + c) = (a * b) + (a * c)A6:
a * (b + c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
0. K
by O, defmultf
;
(a1 * (f . b1)) + (a1 * (f . c1)) =
a1 * ((f . b1) + (f . c1))
by VECTSP_1:def 7
.=
a1 * (f . (b1 + c1))
by VECTSP_1:def 20
.=
a1 * (0. T)
by O, RING_2:6, A5
.=
f . (0. K)
by RING_2:6
;
then A7:
(a1 * (f . b1)) + (a1 * (f . c1)) in rng f
by B0, FUNCT_1:3;
(a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by A1, A3, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(f ") . ((a1 * (f . b1)) + (a1 * (f . c1)))
by A4, A2, A7, defaddf
.=
(f ") . (a1 * ((f . b1) + (f . c1)))
by VECTSP_1:def 7
.=
(f ") . (a1 * (f . (b1 + c1)))
by VECTSP_1:def 20
.=
(f ") . (a1 * (0. T))
by A5, O, RING_2:6
.=
0. K
by Th3
;
hence
a * (b + c) = (a * b) + (a * c)
by A6;
verum end; suppose O:
bc <> 0. K
;
a * (b + c) = (a * b) + (a * c)then A6:
the
multF of
T . (
x,
(f . bc))
in ([#] T) \ (rng f)
by A5, X, Lm4;
the
multF of
T . (
x,
(f . bc)) =
a1 * ((f . b1) + (f . c1))
by A5, VECTSP_1:def 20
.=
(a1 * (f . b1)) + (a1 * (f . c1))
by VECTSP_1:def 7
;
then A7:
not
(a1 * (f . b1)) + (a1 * (f . c1)) in rng f
by A6, XBOOLE_0:def 5;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * (f . bc1)
by O, X, defmultf
.=
a1 * ((f . b1) + (f . c1))
by A5, VECTSP_1:def 20
.=
(a1 * (f . b1)) + (a1 * (f . c1))
by VECTSP_1:def 7
.=
addemb (
f,
ab,
ac)
by A2, A4, A7, defaddf
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A1, A3, defemb
;
verum end; end; suppose Z:
not
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
T by Lm1;
A3:
b + c = (f . b1) + c1
by AS, Y, Z, Lm6;
then reconsider bc =
(f . b1) + c1 as
Element of
carr f by defemb;
A4:
not
bc in [#] K
by A3, AS, Lm6, Z, Y;
A7: the
multF of
T . (
x,
bc) =
a1 * ((f . b1) + c1)
.=
(a1 * (f . b1)) + (a1 * c1)
by VECTSP_1:def 7
;
per cases
( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f )
;
suppose Z1:
the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)then A6:
a * c = a1 * c1
by AS, X, Z, Lm12;
then reconsider ac =
a1 * c1 as
Element of
carr f by defemb;
A9:
not
ac in [#] K
by A6, AS, X, Z, A5, Lm12;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by A3, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f ") . (a1 * ((f . b1) + c1))
by Z1, A4, X, defmultf
.=
addemb (
f,
ab,
ac)
by defaddf, Z1, A7, A2, A9
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by A1, A6, defemb
;
verum end; suppose Z1:
not the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)A9:
( not
x = 0. K & not
bc = 0. K )
by X, A3, AS, Lm6, Z, Y;
A10:
a * (b + c) =
(multemb f) . (
x,
bc)
by A3, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * ((f . b1) + c1)
by X, A4, Z1, A9, defmultf
.=
(a1 * (f . b1)) + (a1 * c1)
by VECTSP_1:def 7
;
per cases
( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f )
;
suppose Z2:
the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)A7:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by X, Z2, Z, defmultf
;
then reconsider ac =
(f ") . (a1 * c1) as
Element of
carr f by defemb;
a1 * c1 in dom (f ")
by Z2, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
ac as
Element of
K ;
(a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by A1, A7, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(a1 * (f . b1)) + (f . ac1)
by defaddf, A2
;
hence
a * (b + c) = (a * b) + (a * c)
by A10, Z2, FUNCT_1:35;
verum end; suppose Z2:
not the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)A9:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by X, Z2, A, BC, Z, defmultf
;
then reconsider ac =
a1 * c1 as
Element of
carr f by defemb;
A8:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by A1, A9, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
a * (b + c)
by defaddf, A2, A7, A8, Z1, A10
;
verum end; end; end; end; suppose Y:
not
y in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider b1 =
b as
Element of
T by Lm1;
per cases
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
K ;
B1:
b + c = b1 + (f . c1)
by AS, Y, Z, Lm6;
then reconsider bc =
b1 + (f . c1) as
Element of
carr f by defemb;
B2:
not
bc in [#] K
by Y, Z, AS, Lm6, B1;
B3:
a * c = a1 * (f . c1)
by AS, X, Z, BC, Lm10;
then reconsider ac =
a1 * (f . c1) as
Element of
carr f by defemb;
B4:
not
ac in [#] K
by B3, X, Z, BC, AS, Lm10;
per cases
( not the multF of T . (x,y) in rng f or the multF of T . (x,y) in rng f )
;
suppose Z1:
not the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B5:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
a1 * b1
by Z1, X, Y, A, BC, defmultf
;
then reconsider ab =
a1 * b1 as
Element of
carr f by defemb;
B6:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
Z3: the
addF of
T . (
ab,
ac) =
(a1 * b1) + (a1 * (f . c1))
.=
a1 * (b1 + (f . c1))
by VECTSP_1:def 7
.=
the
multF of
T . (
x,
bc)
;
per cases
( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f )
;
suppose Z2:
the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)thus a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f ") . (a1 * (b1 + (f . c1)))
by Z2, B2, X, defmultf
.=
addemb (
f,
ab,
ac)
by defaddf, Z2, Z3, B4, B6
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by B3, B5, defemb
;
verum end; suppose Z2:
not the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)B7:
(
x <> 0. K &
bc <> 0. K )
by X, Y, Z, AS, Lm6, B1;
thus a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * (b1 + (f . c1))
by B7, X, B2, Z2, defmultf
.=
addemb (
f,
ab,
ac)
by defaddf, Z2, Z3, B4, B6
.=
(addemb f) . (
ab,
ac)
by defadd
.=
(a * b) + (a * c)
by B3, B5, defemb
;
verum end; end; suppose Z1:
the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B5:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by Z1, X, Y, defmultf
;
a1 * b1 in dom (f ")
by Z1, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
K ;
reconsider ab =
ab1 as
Element of
carr f by B5, defemb;
the
addF of
T . (
(f . ab),
ac)
in ([#] T) \ (rng f)
by Lm3, B4;
then B7:
not the
addF of
T . (
(f . ab),
ac)
in rng f
by XBOOLE_0:def 5;
B10:
(
a <> 0. K &
bc <> 0. K )
by X, Y, Z, AS, Lm6, B1;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B5, B3, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(f . ab1) + (a1 * (f . c1))
by defaddf, B4
.=
(a1 * b1) + (a1 * (f . c1))
by Z1, FUNCT_1:35
.=
a1 * (b1 + (f . c1))
by VECTSP_1:def 7
.=
multemb (
f,
x,
bc)
by B10, X, B2, B9, defmultf
.=
(multemb f) . (
x,
bc)
by defmult
.=
a * (b + c)
by B1, defemb
;
verum end; end; suppose Z:
not
z in [#] K
;
a * (b + c) = (a * b) + (a * c)then reconsider c1 =
c as
Element of
T by Lm1;
per cases
( the addF of T . (y,z) in rng f or not the addF of T . (y,z) in rng f )
;
suppose Z1:
the
addF of
T . (
y,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B1:
b + c =
(addemb f) . (
y,
z)
by defemb
.=
addemb (
f,
y,
z)
by defadd
.=
(f ") . (b1 + c1)
by Y, Z, Z1, defaddf
;
b1 + c1 in dom (f ")
by Z1, FUNCT_1:33;
then
(f ") . (b1 + c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider bc1 =
(f ") . (b1 + c1) as
Element of
K ;
reconsider bc =
bc1 as
Element of
carr f by B1, defemb;
B0:
dom f = [#] K
by FUNCT_2:def 1;
per cases
( bc = 0. K or bc <> 0. K )
;
suppose B5:
bc = 0. K
;
a * (b + c) = (a * b) + (a * c)then B2:
b1 + c1 = 0. T
by Z1, Th2;
B3:
a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
0. K
by B5, defmultf
;
A6:
(a1 * b1) + (a1 * c1) =
a1 * (0. T)
by B2, VECTSP_1:def 7
.=
f . (0. K)
by RING_2:6
;
then A7:
(a1 * b1) + (a1 * c1) in rng f
by B0, FUNCT_1:3;
per cases
( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f )
;
suppose Z2:
the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by Y, X, Z2, defmultf
;
a1 * b1 in dom (f ")
by Z2, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
K ;
reconsider ab =
ab1 as
Element of
carr f by B4, defemb;
U:
f . ((0. K) - ab1) =
(f . (0. K)) - (f . ab1)
by RING_2:8
.=
((a1 * b1) + (a1 * c1)) - (a1 * b1)
by A6, Z2, FUNCT_1:35
.=
(a1 * c1) + ((a1 * b1) - (a1 * b1))
by RLVECT_1:def 3
.=
(a1 * c1) + (0. T)
by RLVECT_1:15
.=
the
multF of
T . (
x,
z)
;
then Z3:
the
multF of
T . (
x,
z)
in rng f
by B0, FUNCT_1:def 3;
B5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by Z, X, Z3, defmultf
;
B11:
a1 * c1 in rng f
by U, B0, FUNCT_1:def 3;
then
a1 * c1 in dom (f ")
by FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B5, defemb;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B5, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
ab1 + ac1
by defaddf
.=
(f ") . ((a1 * b1) + (a1 * c1))
by B11, Z2, Th1
.=
a * (b + c)
by A6, B3, B0, FUNCT_1:34
;
verum end; suppose Z2:
not the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
a1 * b1
by A, BC, Y, X, Z2, defmultf
;
a1 * b1 in ([#] T) \ (rng f)
by Z2, XBOOLE_0:def 5;
then reconsider ab =
a1 * b1 as
Element of
carr f by XBOOLE_0:def 3;
B9:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
Z3:
now not the multF of T . (x,z) in rng fassume Z3:
the
multF of
T . (
x,
z)
in rng f
;
contradictionB5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by Z, X, Z3, defmultf
;
a1 * c1 in dom (f ")
by Z3, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B5, defemb;
B12:
the
addF of
T . (
ab,
(f . ac))
in ([#] T) \ (rng f)
by B9, Lm2;
the
addF of
T . (
ab,
(f . ac))
= (a1 * b1) + (a1 * c1)
by Z3, FUNCT_1:35;
hence
contradiction
by B12, A7, XBOOLE_0:def 5;
verum end; B5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by A, BC, Z, X, Z3, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by Z3, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
B13:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B5, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(f ") . ((a1 * b1) + (a1 * c1))
by A7, B9, B13, defaddf
.=
a * (b + c)
by A6, B3, B0, FUNCT_1:34
;
verum end; end; suppose B5:
bc <> 0. K
;
a * (b + c) = (a * b) + (a * c)then B12:
the
multF of
T . (
x,
(f . bc))
in ([#] T) \ (rng f)
by X, Lm4;
B3:
a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * (f . bc1)
by B5, X, defmultf
.=
a1 * (b1 + c1)
by Z1, FUNCT_1:35
.=
(a1 * b1) + (a1 * c1)
by VECTSP_1:def 7
;
per cases
( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f )
;
suppose Z2:
the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by Y, X, Z2, defmultf
;
a1 * b1 in dom (f ")
by Z2, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
K ;
reconsider ab =
ab1 as
Element of
carr f by B4, defemb;
B8:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by Z, B7, A, BC, X, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by B7, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
B9:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B8, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(f . ab1) + (a1 * c1)
by defaddf, B9
.=
a * (b + c)
by B3, Z2, FUNCT_1:35
;
verum end; suppose Z2:
not the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
a1 * b1
by A, BC, Y, X, Z2, defmultf
;
then reconsider ab =
a1 * b1 as
Element of
carr f by defemb;
B5:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
per cases
( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f )
;
suppose Z3:
the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B8:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by Z, X, Z3, defmultf
;
a1 * c1 in dom (f ")
by Z3, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B8, defemb;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B8, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(a1 * b1) + (f . ac1)
by defaddf, B5
.=
a * (b + c)
by B3, Z3, FUNCT_1:35
;
verum end; suppose Z3:
not the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B8:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by Z, Z3, A, BC, X, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by Z3, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
B9:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
the
multF of
T . (
x,
(f . bc)) =
a1 * (b1 + c1)
by Z1, FUNCT_1:35
.=
(a1 * b1) + (a1 * c1)
by VECTSP_1:def 7
.=
the
addF of
T . (
ab,
ac)
;
then B10:
not the
addF of
T . (
ab,
ac)
in rng f
by B12, XBOOLE_0:def 5;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B8, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
a * (b + c)
by defaddf, B9, B5, B10, B3
;
verum end; end; end; end; suppose Z1:
not the
addF of
T . (
y,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B1:
b + c =
(addemb f) . (
y,
z)
by defemb
.=
addemb (
f,
y,
z)
by defadd
.=
b1 + c1
by Y, Z, Z1, defaddf
;
b1 + c1 in ([#] T) \ (rng f)
by Z1, XBOOLE_0:def 5;
then reconsider bc =
b1 + c1 as
Element of
carr f by XBOOLE_0:def 3;
B2:
not
bc in [#] K
by AS, XBOOLE_0:def 4;
B5:
not
bc = 0. K
by AS, XBOOLE_0:def 4;
per cases
( the multF of T . (x,bc) in rng f or not the multF of T . (x,bc) in rng f )
;
suppose Z2:
the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)B3:
a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
(f ") . (a1 * (b1 + c1))
by Z2, B2, X, defmultf
.=
(f ") . ((a1 * b1) + (a1 * c1))
by VECTSP_1:def 7
;
per cases
( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f )
;
suppose Z3:
the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by Y, X, Z3, defmultf
;
a1 * b1 in dom (f ")
by Z3, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
K ;
reconsider ab =
ab1 as
Element of
carr f by B4, defemb;
B6:
the
multF of
T . (
x,
z)
in rng f
B7:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by X, Z, B6, defmultf
;
a1 * c1 in dom (f ")
by B6, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B7, defemb;
reconsider abr =
a1 * b1 as
Element of
rng f by Z3;
reconsider acr =
a1 * c1 as
Element of
rng f by B6;
B8:
((f ") . abr) + ((f ") . acr) = (f ") . ((a1 * b1) + (a1 * c1))
by Th1;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B7, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
a * (b + c)
by defaddf, B8, B3
;
verum end; suppose Z3:
not the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
a1 * b1
by A, BC, Y, X, Z3, defmultf
;
a1 * b1 in ([#] T) \ (rng f)
by Z3, XBOOLE_0:def 5;
then reconsider ab =
a1 * b1 as
Element of
carr f by XBOOLE_0:def 3;
reconsider ab1 =
ab as
Element of
T ;
B6:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
Z4:
now not the multF of T . (x,z) in rng fassume Z4a:
the
multF of
T . (
x,
z)
in rng f
;
contradictionB7:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by Z4a, X, Z, defmultf
;
a1 * c1 in dom (f ")
by Z4a, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B7, defemb;
U:
the
addF of
T . (
ab,
(f . ac))
in ([#] T) \ (rng f)
by B6, Lm2;
f . ac1 = a1 * c1
by Z4a, FUNCT_1:35;
then ab1 + (f . ac1) =
a1 * (b1 + c1)
by VECTSP_1:def 7
.=
the
multF of
T . (
x,
bc)
;
hence
contradiction
by U, Z2, XBOOLE_0:def 5;
verum end; B7:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by Z4, A, BC, X, Z, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by Z4, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
reconsider ac1 =
ac as
Element of
T ;
B9:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
B10:
(a1 * b1) + (a1 * c1) =
a1 * (b1 + c1)
by VECTSP_1:def 7
.=
the
multF of
T . (
x,
bc)
;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B7, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
a * (b + c)
by defaddf, B6, B9, B10, Z2, B3
;
verum end; end; suppose Z2:
not the
multF of
T . (
x,
bc)
in rng f
;
a * (b + c) = (a * b) + (a * c)B3:
a * (b + c) =
(multemb f) . (
x,
bc)
by B1, defemb
.=
multemb (
f,
x,
bc)
by defmult
.=
a1 * (b1 + c1)
by A, Z2, B2, B5, X, defmultf
.=
(a1 * b1) + (a1 * c1)
by VECTSP_1:def 7
;
per cases
( the multF of T . (x,y) in rng f or not the multF of T . (x,y) in rng f )
;
suppose Z3:
the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
(f ") . (a1 * b1)
by Y, X, Z3, defmultf
;
a1 * b1 in dom (f ")
by Z3, FUNCT_1:33;
then
(f ") . (a1 * b1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ab1 =
(f ") . (a1 * b1) as
Element of
K ;
reconsider ab =
ab1 as
Element of
carr f by B4, defemb;
B5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by A, BC, Z, X, Z4, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by Z4, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
B9:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B5, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(f . ab1) + (a1 * c1)
by defaddf, B9
.=
a * (b + c)
by B3, Z3, FUNCT_1:35
;
verum end; suppose Z3:
not the
multF of
T . (
x,
y)
in rng f
;
a * (b + c) = (a * b) + (a * c)B4:
a * b =
(multemb f) . (
x,
y)
by defemb
.=
multemb (
f,
x,
y)
by defmult
.=
a1 * b1
by A, BC, Y, X, Z3, defmultf
;
a1 * b1 in ([#] T) \ (rng f)
by Z3, XBOOLE_0:def 5;
then reconsider ab =
a1 * b1 as
Element of
carr f by XBOOLE_0:def 3;
B9:
not
ab in [#] K
by AS, XBOOLE_0:def 4;
per cases
( the multF of T . (x,z) in rng f or not the multF of T . (x,z) in rng f )
;
suppose Z4:
the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
(f ") . (a1 * c1)
by Z, X, Z4, defmultf
;
a1 * c1 in dom (f ")
by Z4, FUNCT_1:33;
then
(f ") . (a1 * c1) in rng (f ")
by FUNCT_1:def 3;
then reconsider ac1 =
(f ") . (a1 * c1) as
Element of
K ;
reconsider ac =
ac1 as
Element of
carr f by B5, defemb;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B5, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
(a1 * b1) + (f . ac1)
by defaddf, B9
.=
a * (b + c)
by B3, Z4, FUNCT_1:35
;
verum end; suppose Z4:
not the
multF of
T . (
x,
z)
in rng f
;
a * (b + c) = (a * b) + (a * c)B5:
a * c =
(multemb f) . (
x,
z)
by defemb
.=
multemb (
f,
x,
z)
by defmult
.=
a1 * c1
by A, BC, Z, X, Z4, defmultf
;
a1 * c1 in ([#] T) \ (rng f)
by Z4, XBOOLE_0:def 5;
then reconsider ac =
a1 * c1 as
Element of
carr f by XBOOLE_0:def 3;
B19:
not
ac in [#] K
by AS, XBOOLE_0:def 4;
B20: the
addF of
T . (
ab,
ac) =
(a1 * b1) + (a1 * c1)
.=
a1 * (b1 + c1)
by VECTSP_1:def 7
.=
the
multF of
T . (
x,
bc)
;
thus (a * b) + (a * c) =
(addemb f) . (
ab,
ac)
by B4, B5, defemb
.=
addemb (
f,
ab,
ac)
by defadd
.=
a * (b + c)
by Z2, B3, B9, B19, B20, defaddf
;
verum end; end; end; end; end; end; end;
end; thus (b + c) * a =
a * (b + c)
by GROUP_1:def 12
.=
(b * a) + (a * c)
by I, GROUP_1:def 12
.=
(b * a) + (c * a)
by GROUP_1:def 12
;
verum end; end;
hence
embField f is distributive
; verum