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, Th11
.=
QClass. (pmult (padd x,y),z)
by Th12
;
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 5;
then reconsider s2 = [((y `1 ) * (z `1 )),((y `2 ) * (z `2 ))] as Element of Q. I by Def1;
A8:
x `2 <> 0. I
by Th2;
then A9:
(x `2 ) * (y `2 ) <> 0. I
by A6, VECTSP_2:def 5;
then reconsider s = [(((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))),((x `2 ) * (y `2 ))] as Element of Q. I by Def1;
A10:
(x `2 ) * (z `2 ) <> 0. I
by A8, A5, VECTSP_2:def 5;
then reconsider s1 = [((x `1 ) * (z `1 )),((x `2 ) * (z `2 ))] as Element of Q. I by Def1;
((x `2 ) * (z `2 )) * ((y `2 ) * (z `2 )) <> 0. I
by A7, A10, VECTSP_2:def 5;
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;
((x `2 ) * (y `2 )) * (z `2 ) <> 0. I
by A5, A9, VECTSP_2:def 5;
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;
A11: padd (pmult x,z),(pmult y,z) =
[((((x `1 ) * (z `1 )) * (s2 `2 )) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * (s2 `2 ))]
by MCART_1:def 1
.=
[((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * (s2 `2 ))]
by MCART_1:def 2
.=
[((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * ((y `2 ) * (z `2 )))]
by MCART_1:def 2
.=
[((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `1 )) * (s1 `2 ))),((s1 `2 ) * ((y `2 ) * (z `2 )))]
by MCART_1:def 1
.=
[((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `1 )) * ((x `2 ) * (z `2 )))),((s1 `2 ) * ((y `2 ) * (z `2 )))]
by MCART_1:def 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 )))]
by MCART_1:def 2
;
A12: pmult (padd x,y),z =
[((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )),((s `2 ) * (z `2 ))]
by MCART_1:def 1
.=
[((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )),(((x `2 ) * (y `2 )) * (z `2 ))]
by MCART_1:def 2
;
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 MCART_1:def 2;
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 MCART_1:def 1;
((t `1 ) * (((x `2 ) * (y `2 )) * (z `2 ))) * (z `2 ) =
(t `1 ) * ((((x `2 ) * (y `2 )) * (z `2 )) * (z `2 ))
by GROUP_1:def 4
.=
(t `1 ) * (((x `2 ) * ((y `2 ) * (z `2 ))) * (z `2 ))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `1 )) * ((x `2 ) * (z `2 ))))
by A14, GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (z `1 )) * (y `2 )) * (z `2 )) + (((y `1 ) * (z `1 )) * ((x `2 ) * (z `2 ))))
by GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (z `1 )) * (y `2 )) * (z `2 )) + ((((y `1 ) * (z `1 )) * (x `2 )) * (z `2 )))
by GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (z `1 )) * (y `2 )) + (((y `1 ) * (z `1 )) * (x `2 ))) * (z `2 ))
by VECTSP_1:def 12
.=
(t `2 ) * ((((z `1 ) * ((x `1 ) * (y `2 ))) + (((y `1 ) * (z `1 )) * (x `2 ))) * (z `2 ))
by GROUP_1:def 4
.=
(t `2 ) * ((((z `1 ) * ((x `1 ) * (y `2 ))) + ((z `1 ) * ((y `1 ) * (x `2 )))) * (z `2 ))
by GROUP_1:def 4
.=
(t `2 ) * (((z `1 ) * (((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 )))) * (z `2 ))
by VECTSP_1:def 11
.=
((t `2 ) * ((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 ))) * (z `2 )
by GROUP_1:def 4
;
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 MCART_1:def 2
.=
(t `2 ) * (r `1 )
by MCART_1:def 1
;
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 MCART_1:def 2;
then A16:
(t `1 ) * (((x `2 ) * (y `2 )) * (z `2 )) = (t `2 ) * ((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 ))
by MCART_1:def 1;
(t `1 ) * (s3 `2 ) =
(t `1 ) * (((x `2 ) * (z `2 )) * ((y `2 ) * (z `2 )))
by MCART_1:def 2
.=
(t `1 ) * ((((x `2 ) * (z `2 )) * (y `2 )) * (z `2 ))
by GROUP_1:def 4
.=
((t `1 ) * (((x `2 ) * (z `2 )) * (y `2 ))) * (z `2 )
by GROUP_1:def 4
.=
((t `1 ) * (((x `2 ) * (y `2 )) * (z `2 ))) * (z `2 )
by GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (y `2 )) + ((y `1 ) * (x `2 ))) * (z `1 )) * (z `2 ))
by A16, GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (y `2 )) * (z `1 )) + (((y `1 ) * (x `2 )) * (z `1 ))) * (z `2 ))
by VECTSP_1:def 12
.=
(t `2 ) * (((((x `1 ) * (y `2 )) * (z `1 )) * (z `2 )) + ((((y `1 ) * (x `2 )) * (z `1 )) * (z `2 )))
by VECTSP_1:def 12
.=
(t `2 ) * ((((y `2 ) * ((x `1 ) * (z `1 ))) * (z `2 )) + ((((y `1 ) * (x `2 )) * (z `1 )) * (z `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + ((((y `1 ) * (x `2 )) * (z `1 )) * (z `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + ((((y `1 ) * (z `1 )) * (x `2 )) * (z `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (z `1 )) * ((y `2 ) * (z `2 ))) + (((y `1 ) * (z `1 )) * ((x `2 ) * (z `2 ))))
by GROUP_1:def 4
.=
(t `2 ) * (s3 `1 )
by MCART_1:def 1
;
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, Th12
.=
qadd (QClass. (pmult x,z)),(QClass. (pmult y,z))
by Th12
.=
QClass. (padd (pmult x,z),(pmult y,z))
by Th11
;
hence
qmult (qadd u,v),w = qadd (qmult u,w),(qmult v,w)
by A4, A15, A13, SUBSET_1:8; verum