let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Q. I holds qmult (QClass. u),(QClass. v) = QClass. (pmult u,v)
let u, v be Element of Q. I; :: thesis: qmult (QClass. u),(QClass. v) = QClass. (pmult u,v)
( u `2 <> 0. I & v `2 <> 0. I )
by Th2;
then
(u `2 ) * (v `2 ) <> 0. I
by VECTSP_2:def 5;
then reconsider w = [((u `1 ) * (v `1 )),((u `2 ) * (v `2 ))] as Element of Q. I by Def1;
A1:
w `1 = (u `1 ) * (v `1 )
by MCART_1:def 1;
A2:
w `2 = (u `2 ) * (v `2 )
by MCART_1:def 2;
A3:
for z being Element of Q. I st z in QClass. (pmult u,v) holds
z in qmult (QClass. u),(QClass. v)
for z being Element of Q. I st z in qmult (QClass. u),(QClass. v) holds
z in QClass. (pmult u,v)
proof
let z be
Element of
Q. I;
:: thesis: ( z in qmult (QClass. u),(QClass. v) implies z in QClass. (pmult u,v) )
assume
z in qmult (QClass. u),
(QClass. v)
;
:: thesis: z in QClass. (pmult u,v)
then consider a,
b being
Element of
Q. I such that A5:
(
a in QClass. u &
b in QClass. v &
(z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) )
by Def7;
A6:
(a `1 ) * (u `2 ) = (a `2 ) * (u `1 )
by A5, Def4;
A7:
(b `1 ) * (v `2 ) = (b `2 ) * (v `1 )
by A5, Def4;
now per cases
( a `1 = 0. I or b `1 = 0. I or ( a `1 <> 0. I & b `1 <> 0. I ) )
;
case A8:
a `1 = 0. I
;
:: thesis: z in QClass. (pmult u,v)then A9:
(a `1 ) * (u `2 ) = 0. I
by VECTSP_1:39;
A10:
(
a `2 <> 0. I &
b `2 <> 0. I )
by Th2;
then A11:
u `1 = 0. I
by A6, A9, VECTSP_2:def 5;
(a `1 ) * (b `1 ) = 0. I
by A8, VECTSP_1:39;
then A12:
(z `2 ) * ((a `1 ) * (b `1 )) = 0. I
by VECTSP_1:39;
(a `2 ) * (b `2 ) <> 0. I
by A10, VECTSP_2:def 5;
then A13:
z `1 = 0. I
by A5, A12, VECTSP_2:def 5;
(z `2 ) * ((u `1 ) * (v `1 )) =
(z `2 ) * (0. I)
by A11, VECTSP_1:39
.=
0. I
by VECTSP_1:39
.=
(z `1 ) * ((u `2 ) * (v `2 ))
by A13, VECTSP_1:39
;
hence
z in QClass. (pmult u,v)
by A1, A2, Def4;
:: thesis: verum end; case A14:
b `1 = 0. I
;
:: thesis: z in QClass. (pmult u,v)then A15:
(b `1 ) * (v `2 ) = 0. I
by VECTSP_1:39;
A16:
(
a `2 <> 0. I &
b `2 <> 0. I )
by Th2;
then A17:
v `1 = 0. I
by A7, A15, VECTSP_2:def 5;
(a `1 ) * (b `1 ) = 0. I
by A14, VECTSP_1:39;
then A18:
(z `2 ) * ((a `1 ) * (b `1 )) = 0. I
by VECTSP_1:39;
(a `2 ) * (b `2 ) <> 0. I
by A16, VECTSP_2:def 5;
then A19:
z `1 = 0. I
by A5, A18, VECTSP_2:def 5;
(z `2 ) * ((u `1 ) * (v `1 )) =
(z `2 ) * (0. I)
by A17, VECTSP_1:39
.=
0. I
by VECTSP_1:39
.=
(z `1 ) * ((u `2 ) * (v `2 ))
by A19, VECTSP_1:39
;
hence
z in QClass. (pmult u,v)
by A1, A2, Def4;
:: thesis: verum end; case A20:
(
a `1 <> 0. I &
b `1 <> 0. I )
;
:: thesis: z in QClass. (pmult u,v)A21:
a `1 divides (a `2 ) * (u `1 )
by A6, GCD_1:def 1;
then A22:
u `2 = ((a `2 ) * (u `1 )) / (a `1 )
by A6, A20, GCD_1:def 4;
A23:
b `1 divides (b `2 ) * (v `1 )
by A7, GCD_1:def 1;
then A24:
v `2 = ((b `2 ) * (v `1 )) / (b `1 )
by A7, A20, GCD_1:def 4;
A25:
(a `1 ) * (b `1 ) <> 0. I
by A20, VECTSP_2:def 5;
A26:
(a `1 ) * (b `1 ) divides ((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 ))
by A21, A23, GCD_1:3;
then A27:
(a `1 ) * (b `1 ) divides (z `1 ) * (((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 )))
by GCD_1:7;
(a `1 ) * (b `1 ) divides (a `1 ) * (b `1 )
;
then A28:
(a `1 ) * (b `1 ) divides (((z `2 ) * (u `1 )) * (v `1 )) * ((a `1 ) * (b `1 ))
by GCD_1:7;
(z `1 ) * ((u `2 ) * (v `2 )) =
(z `1 ) * ((((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 ))) / ((a `1 ) * (b `1 )))
by A20, A21, A22, A23, A24, GCD_1:14
.=
((z `1 ) * (((a `2 ) * (u `1 )) * ((b `2 ) * (v `1 )))) / ((a `1 ) * (b `1 ))
by A25, A26, A27, GCD_1:11
.=
((z `1 ) * ((((u `1 ) * (a `2 )) * (b `2 )) * (v `1 ))) / ((a `1 ) * (b `1 ))
by GROUP_1:def 4
.=
((z `1 ) * ((((a `2 ) * (b `2 )) * (u `1 )) * (v `1 ))) / ((a `1 ) * (b `1 ))
by GROUP_1:def 4
.=
(((z `1 ) * (((a `2 ) * (b `2 )) * (u `1 ))) * (v `1 )) / ((a `1 ) * (b `1 ))
by GROUP_1:def 4
.=
((((z `2 ) * ((a `1 ) * (b `1 ))) * (u `1 )) * (v `1 )) / ((a `1 ) * (b `1 ))
by A5, GROUP_1:def 4
.=
((((z `2 ) * (u `1 )) * ((a `1 ) * (b `1 ))) * (v `1 )) / ((a `1 ) * (b `1 ))
by GROUP_1:def 4
.=
((((z `2 ) * (u `1 )) * (v `1 )) * ((a `1 ) * (b `1 ))) / ((a `1 ) * (b `1 ))
by GROUP_1:def 4
.=
(((z `2 ) * (u `1 )) * (v `1 )) * (((a `1 ) * (b `1 )) / ((a `1 ) * (b `1 )))
by A25, A28, GCD_1:11
.=
(((z `2 ) * (u `1 )) * (v `1 )) * (1_ I)
by A25, GCD_1:9
.=
((z `2 ) * (u `1 )) * (v `1 )
by VECTSP_1:def 13
.=
(z `2 ) * ((u `1 ) * (v `1 ))
by GROUP_1:def 4
;
hence
z in QClass. (pmult u,v)
by A1, A2, Def4;
:: thesis: verum end;
hence
z in QClass. (pmult u,v)
;
:: thesis: verum
end;
hence
qmult (QClass. u),(QClass. v) = QClass. (pmult u,v)
by A3, SUBSET_1:8; :: thesis: verum