let I be non degenerated commutative domRing-like Ring; for u, v, w being Element of Quot. I holds qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
let u, v, w be Element of Quot. I; qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
consider x being Element of Q. I such that
A1:
u = QClass. x
by Def5;
consider y being Element of Q. I such that
A2:
v = QClass. y
by Def5;
consider z being Element of Q. I such that
A3:
w = QClass. z
by Def5;
A4: qmult ((qadd (u,v)),w) =
qmult ((QClass. (padd (x,y))),(QClass. z))
by A1, A2, A3, Th9
.=
QClass. (pmult ((padd (x,y)),z))
by Th10
;
A5:
z `2 <> 0. I
by Th2;
A6:
y `2 <> 0. I
by Th2;
then A7:
(y `2) * (z `2) <> 0. I
by A5, VECTSP_2:def 1;
then reconsider s2 = [((y `1) * (z `1)),((y `2) * (z `2))] as Element of Q. I by Def1;
X2:
( [((y `1) * (z `1)),((y `2) * (z `2))] `1 = (y `1) * (z `1) & [((y `1) * (z `1)),((y `2) * (z `2))] `2 = (y `2) * (z `2) )
;
A8:
x `2 <> 0. I
by Th2;
then A9:
(x `2) * (y `2) <> 0. I
by A6, VECTSP_2:def 1;
then reconsider s = [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
X:
( [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `1 = ((x `1) * (y `2)) + ((y `1) * (x `2)) & [(((x `1) * (y `2)) + ((y `1) * (x `2))),((x `2) * (y `2))] `2 = (x `2) * (y `2) )
;
A10:
(x `2) * (z `2) <> 0. I
by A8, A5, VECTSP_2:def 1;
then reconsider s1 = [((x `1) * (z `1)),((x `2) * (z `2))] as Element of Q. I by Def1;
X1:
( [((x `1) * (z `1)),((x `2) * (z `2))] `1 = (x `1) * (z `1) & [((x `1) * (z `1)),((x `2) * (z `2))] `2 = (x `2) * (z `2) )
;
((x `2) * (z `2)) * ((y `2) * (z `2)) <> 0. I
by A7, A10, VECTSP_2:def 1;
then reconsider s3 = [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] as Element of Q. I by Def1;
X3:
( [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] `1 = (((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2))) & [((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))] `2 = ((x `2) * (z `2)) * ((y `2) * (z `2)) )
;
((x `2) * (y `2)) * (z `2) <> 0. I
by A5, A9, VECTSP_2:def 1;
then reconsider r = [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] as Element of Q. I by Def1;
Y:
( [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] `1 = (((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1) & [((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))] `2 = ((x `2) * (y `2)) * (z `2) )
;
A11: padd ((pmult (x,z)),(pmult (y,z))) =
[((((x `1) * (z `1)) * (s2 `2)) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))]
by X1
.=
[((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * (s2 `2))]
by X2
.=
[((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((s2 `1) * (s1 `2))),((s1 `2) * ((y `2) * (z `2)))]
by X2
.=
[((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * (s1 `2))),((s1 `2) * ((y `2) * (z `2)))]
by X2
.=
[((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),((s1 `2) * ((y `2) * (z `2)))]
by X1
.=
[((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2)))),(((x `2) * (z `2)) * ((y `2) * (z `2)))]
by X1
;
A12: pmult ((padd (x,y)),z) =
[((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),((s `2) * (z `2))]
by X
.=
[((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)),(((x `2) * (y `2)) * (z `2))]
by X
;
A13:
for t being Element of Q. I st t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) holds
t in QClass. (pmult ((padd (x,y)),z))
proof
let t be
Element of
Q. I;
( t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) implies t in QClass. (pmult ((padd (x,y)),z)) )
assume
t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
;
t in QClass. (pmult ((padd (x,y)),z))
then
(t `1) * (s3 `2) = (t `2) * (s3 `1)
by A11, Def4;
then
(t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2))) = (t `2) * (s3 `1)
by X3;
then A14:
(t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2))) = (t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2))))
by X3;
((t `1) * (((x `2) * (y `2)) * (z `2))) * (z `2) =
(t `1) * ((((x `2) * (y `2)) * (z `2)) * (z `2))
by GROUP_1:def 3
.=
(t `1) * (((x `2) * ((y `2) * (z `2))) * (z `2))
by GROUP_1:def 3
.=
(t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2))))
by A14, GROUP_1:def 3
.=
(t `2) * (((((x `1) * (z `1)) * (y `2)) * (z `2)) + (((y `1) * (z `1)) * ((x `2) * (z `2))))
by GROUP_1:def 3
.=
(t `2) * (((((x `1) * (z `1)) * (y `2)) * (z `2)) + ((((y `1) * (z `1)) * (x `2)) * (z `2)))
by GROUP_1:def 3
.=
(t `2) * (((((x `1) * (z `1)) * (y `2)) + (((y `1) * (z `1)) * (x `2))) * (z `2))
by VECTSP_1:def 3
.=
(t `2) * ((((z `1) * ((x `1) * (y `2))) + (((y `1) * (z `1)) * (x `2))) * (z `2))
by GROUP_1:def 3
.=
(t `2) * ((((z `1) * ((x `1) * (y `2))) + ((z `1) * ((y `1) * (x `2)))) * (z `2))
by GROUP_1:def 3
.=
(t `2) * (((z `1) * (((x `1) * (y `2)) + ((y `1) * (x `2)))) * (z `2))
by VECTSP_1:def 2
.=
((t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1))) * (z `2)
by GROUP_1:def 3
;
then
(t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1))
by A5, GCD_1:1;
then (t `1) * (r `2) =
(t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1))
by Y
.=
(t `2) * (r `1)
by Y
;
hence
t in QClass. (pmult ((padd (x,y)),z))
by A12, Def4;
verum
end;
A15:
for t being Element of Q. I st t in QClass. (pmult ((padd (x,y)),z)) holds
t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
proof
let t be
Element of
Q. I;
( t in QClass. (pmult ((padd (x,y)),z)) implies t in QClass. (padd ((pmult (x,z)),(pmult (y,z)))) )
assume
t in QClass. (pmult ((padd (x,y)),z))
;
t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
then
(t `1) * (r `2) = (t `2) * (r `1)
by A12, Def4;
then
(t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * (r `1)
by Y;
then A16:
(t `1) * (((x `2) * (y `2)) * (z `2)) = (t `2) * ((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1))
by Y;
(t `1) * (s3 `2) =
(t `1) * (((x `2) * (z `2)) * ((y `2) * (z `2)))
by X3
.=
(t `1) * ((((x `2) * (z `2)) * (y `2)) * (z `2))
by GROUP_1:def 3
.=
((t `1) * (((x `2) * (z `2)) * (y `2))) * (z `2)
by GROUP_1:def 3
.=
((t `1) * (((x `2) * (y `2)) * (z `2))) * (z `2)
by GROUP_1:def 3
.=
(t `2) * (((((x `1) * (y `2)) + ((y `1) * (x `2))) * (z `1)) * (z `2))
by A16, GROUP_1:def 3
.=
(t `2) * (((((x `1) * (y `2)) * (z `1)) + (((y `1) * (x `2)) * (z `1))) * (z `2))
by VECTSP_1:def 3
.=
(t `2) * (((((x `1) * (y `2)) * (z `1)) * (z `2)) + ((((y `1) * (x `2)) * (z `1)) * (z `2)))
by VECTSP_1:def 3
.=
(t `2) * ((((y `2) * ((x `1) * (z `1))) * (z `2)) + ((((y `1) * (x `2)) * (z `1)) * (z `2)))
by GROUP_1:def 3
.=
(t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((((y `1) * (x `2)) * (z `1)) * (z `2)))
by GROUP_1:def 3
.=
(t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + ((((y `1) * (z `1)) * (x `2)) * (z `2)))
by GROUP_1:def 3
.=
(t `2) * ((((x `1) * (z `1)) * ((y `2) * (z `2))) + (((y `1) * (z `1)) * ((x `2) * (z `2))))
by GROUP_1:def 3
.=
(t `2) * (s3 `1)
by X3
;
hence
t in QClass. (padd ((pmult (x,z)),(pmult (y,z))))
by A11, Def4;
verum
end;
qadd ((qmult (u,w)),(qmult (v,w))) =
qadd ((QClass. (pmult (x,z))),(qmult ((QClass. y),(QClass. z))))
by A1, A2, A3, Th10
.=
qadd ((QClass. (pmult (x,z))),(QClass. (pmult (y,z))))
by Th10
.=
QClass. (padd ((pmult (x,z)),(pmult (y,z))))
by Th9
;
hence
qmult ((qadd (u,v)),w) = qadd ((qmult (u,w)),(qmult (v,w)))
by A4, A15, A13, SUBSET_1:3; verum