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 5;
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 5;
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 5;
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 5;
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 5;
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: padd (pmult x,y),(pmult x,z) =
[((((x `1 ) * (y `1 )) * (s2 `2 )) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * (s2 `2 ))]
by MCART_1:def 1
.=
[((((x `1 ) * (y `1 )) * ((x `2 ) * (z `2 ))) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * (s2 `2 ))]
by MCART_1:def 2
.=
[((((x `1 ) * (y `1 )) * ((x `2 ) * (z `2 ))) + ((s2 `1 ) * (s1 `2 ))),((s1 `2 ) * ((x `2 ) * (z `2 )))]
by MCART_1:def 2
.=
[((((x `1 ) * (y `1 )) * ((x `2 ) * (z `2 ))) + (((x `1 ) * (z `1 )) * (s1 `2 ))),((s1 `2 ) * ((x `2 ) * (z `2 )))]
by MCART_1:def 1
.=
[((((x `1 ) * (y `1 )) * ((x `2 ) * (z `2 ))) + (((x `1 ) * (z `1 )) * ((x `2 ) * (y `2 )))),((s1 `2 ) * ((x `2 ) * (z `2 )))]
by MCART_1:def 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 )))]
by MCART_1:def 2
;
A11: pmult x,(padd y,z) =
[((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 )))),((x `2 ) * (s `2 ))]
by MCART_1:def 1
.=
[((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 )))),((x `2 ) * ((y `2 ) * (z `2 )))]
by MCART_1:def 2
;
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 MCART_1:def 2;
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 MCART_1:def 1;
((t `1 ) * ((x `2 ) * ((y `2 ) * (z `2 )))) * (x `2 ) =
((t `1 ) * (((x `2 ) * (y `2 )) * (z `2 ))) * (x `2 )
by GROUP_1:def 4
.=
(t `1 ) * ((((x `2 ) * (y `2 )) * (z `2 )) * (x `2 ))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (y `1 )) * ((x `2 ) * (z `2 ))) + (((x `1 ) * (z `1 )) * ((x `2 ) * (y `2 ))))
by A13, GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (y `1 )) * (z `2 )) * (x `2 )) + (((x `1 ) * (z `1 )) * ((x `2 ) * (y `2 ))))
by GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (y `1 )) * (z `2 )) * (x `2 )) + ((((x `1 ) * (z `1 )) * (y `2 )) * (x `2 )))
by GROUP_1:def 4
.=
(t `2 ) * (((((x `1 ) * (y `1 )) * (z `2 )) + (((x `1 ) * (z `1 )) * (y `2 ))) * (x `2 ))
by VECTSP_1:def 12
.=
(t `2 ) * ((((x `1 ) * ((y `1 ) * (z `2 ))) + (((x `1 ) * (z `1 )) * (y `2 ))) * (x `2 ))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * ((y `1 ) * (z `2 ))) + ((x `1 ) * ((z `1 ) * (y `2 )))) * (x `2 ))
by GROUP_1:def 4
.=
(t `2 ) * (((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 )))) * (x `2 ))
by VECTSP_1:def 11
.=
((t `2 ) * ((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 ))))) * (x `2 )
by GROUP_1:def 4
;
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 MCART_1:def 2
.=
(t `2 ) * (r `1 )
by MCART_1:def 1
;
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 MCART_1:def 2;
then A15:
(t `1 ) * ((x `2 ) * ((y `2 ) * (z `2 ))) = (t `2 ) * ((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 ))))
by MCART_1:def 1;
(t `1 ) * (s3 `2 ) =
(t `1 ) * (((x `2 ) * (y `2 )) * ((x `2 ) * (z `2 )))
by MCART_1:def 2
.=
(t `1 ) * ((((x `2 ) * (y `2 )) * (z `2 )) * (x `2 ))
by GROUP_1:def 4
.=
((t `1 ) * (((x `2 ) * (y `2 )) * (z `2 ))) * (x `2 )
by GROUP_1:def 4
.=
((t `2 ) * ((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 ))))) * (x `2 )
by A15, GROUP_1:def 4
.=
(t `2 ) * (((x `1 ) * (((y `1 ) * (z `2 )) + ((z `1 ) * (y `2 )))) * (x `2 ))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * ((y `1 ) * (z `2 ))) + ((x `1 ) * ((z `1 ) * (y `2 )))) * (x `2 ))
by VECTSP_1:def 11
.=
(t `2 ) * ((((x `1 ) * ((y `1 ) * (z `2 ))) * (x `2 )) + (((x `1 ) * ((z `1 ) * (y `2 ))) * (x `2 )))
by VECTSP_1:def 12
.=
(t `2 ) * (((((x `1 ) * (y `1 )) * (z `2 )) * (x `2 )) + (((x `1 ) * ((z `1 ) * (y `2 ))) * (x `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (y `1 )) * ((z `2 ) * (x `2 ))) + (((x `1 ) * ((z `1 ) * (y `2 ))) * (x `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (y `1 )) * ((z `2 ) * (x `2 ))) + ((((x `1 ) * (z `1 )) * (y `2 )) * (x `2 )))
by GROUP_1:def 4
.=
(t `2 ) * ((((x `1 ) * (y `1 )) * ((z `2 ) * (x `2 ))) + (((x `1 ) * (z `1 )) * ((y `2 ) * (x `2 ))))
by GROUP_1:def 4
.=
(t `2 ) * (s3 `1 )
by MCART_1:def 1
;
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, Th11
.=
QClass. (pmult x,(padd y,z))
by Th12
;
qadd (qmult u,v),(qmult u,w) =
qadd (QClass. (pmult x,y)),(qmult (QClass. x),(QClass. z))
by A1, A2, A3, Th12
.=
qadd (QClass. (pmult x,y)),(QClass. (pmult x,z))
by Th12
.=
QClass. (padd (pmult x,y),(pmult x,z))
by Th11
;
hence
qmult u,(qadd v,w) = qadd (qmult u,v),(qmult u,w)
by A16, A14, A12, SUBSET_1:8; verum