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