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;
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;
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;
((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;
(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;
A10:
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 Def4;
then
(t `1) * (((x `2) * (y `2)) * ((x `2) * (z `2))) = (t `2) * (s3 `1)
;
then A11:
(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))))
;
((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 A11, 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))))
.=
(t `2) * (r `1)
;
hence
t in QClass. (pmult (x,(padd (y,z))))
by Def4;
verum
end;
A12:
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 Def4;
then
(t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * (r `1)
;
then A13:
(t `1) * ((x `2) * ((y `2) * (z `2))) = (t `2) * ((x `1) * (((y `1) * (z `2)) + ((z `1) * (y `2))))
;
(t `1) * (s3 `2) =
(t `1) * (((x `2) * (y `2)) * ((x `2) * (z `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) * (z `2)) + ((z `1) * (y `2))))) * (x `2)
by A13, 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)
;
hence
t in QClass. (padd ((pmult (x,y)),(pmult (x,z))))
by Def4;
verum
end;
A14: 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 A14, A12, A10, SUBSET_1:3; verum