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 1;
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) & w `2 = (u `2) * (v `2) ) ;
A2: 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
A3: a in QClass. u and
A4: b in QClass. v and
A5: (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) by Def7;
A6: (b `1) * (v `2) = (b `2) * (v `1) by A4, Def4;
A7: (a `1) * (u `2) = (a `2) * (u `1) by A3, Def4;
now :: thesis: ( ( a `1 = 0. I & z in QClass. (pmult (u,v)) ) or ( b `1 = 0. I & z in QClass. (pmult (u,v)) ) or ( a `1 <> 0. I & b `1 <> 0. I & z in QClass. (pmult (u,v)) ) )
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 (a `1) * (b `1) = 0. I ;
then A9: (z `2) * ((a `1) * (b `1)) = 0. I ;
A10: a `2 <> 0. I by Th2;
b `2 <> 0. I by Th2;
then (a `2) * (b `2) <> 0. I by A10, VECTSP_2:def 1;
then A11: z `1 = 0. I by A5, A9, VECTSP_2:def 1;
(a `1) * (u `2) = 0. I by A8;
then u `1 = 0. I by A7, A10, VECTSP_2:def 1;
then (z `2) * ((u `1) * (v `1)) = (z `2) * (0. I)
.= 0. I
.= (z `1) * ((u `2) * (v `2)) by A11 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; :: thesis: verum
end;
case A12: b `1 = 0. I ; :: thesis: z in QClass. (pmult (u,v))
then (a `1) * (b `1) = 0. I ;
then A13: (z `2) * ((a `1) * (b `1)) = 0. I ;
A14: b `2 <> 0. I by Th2;
a `2 <> 0. I by Th2;
then (a `2) * (b `2) <> 0. I by A14, VECTSP_2:def 1;
then A15: z `1 = 0. I by A5, A13, VECTSP_2:def 1;
(b `1) * (v `2) = 0. I by A12;
then v `1 = 0. I by A6, A14, VECTSP_2:def 1;
then (z `2) * ((u `1) * (v `1)) = (z `2) * (0. I)
.= 0. I
.= (z `1) * ((u `2) * (v `2)) by A15 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; :: thesis: verum
end;
case A16: ( a `1 <> 0. I & b `1 <> 0. I ) ; :: thesis: z in QClass. (pmult (u,v))
(a `1) * (b `1) divides (a `1) * (b `1) ;
then A17: (a `1) * (b `1) divides (((z `2) * (u `1)) * (v `1)) * ((a `1) * (b `1)) by GCD_1:7;
A18: (a `1) * (b `1) <> 0. I by A16, VECTSP_2:def 1;
A19: b `1 divides (b `2) * (v `1) by A6, GCD_1:def 1;
then A20: v `2 = ((b `2) * (v `1)) / (b `1) by A6, A16, GCD_1:def 4;
A21: a `1 divides (a `2) * (u `1) by A7, GCD_1:def 1;
then A22: (a `1) * (b `1) divides ((a `2) * (u `1)) * ((b `2) * (v `1)) by A19, GCD_1:3;
then A23: (a `1) * (b `1) divides (z `1) * (((a `2) * (u `1)) * ((b `2) * (v `1))) by GCD_1:7;
u `2 = ((a `2) * (u `1)) / (a `1) by A7, A16, A21, GCD_1:def 4;
then (z `1) * ((u `2) * (v `2)) = (z `1) * ((((a `2) * (u `1)) * ((b `2) * (v `1))) / ((a `1) * (b `1))) by A16, A21, A19, A20, GCD_1:14
.= ((z `1) * (((a `2) * (u `1)) * ((b `2) * (v `1)))) / ((a `1) * (b `1)) by A18, A22, A23, GCD_1:11
.= ((z `1) * ((((u `1) * (a `2)) * (b `2)) * (v `1))) / ((a `1) * (b `1)) by GROUP_1:def 3
.= ((z `1) * ((((a `2) * (b `2)) * (u `1)) * (v `1))) / ((a `1) * (b `1)) by GROUP_1:def 3
.= (((z `1) * (((a `2) * (b `2)) * (u `1))) * (v `1)) / ((a `1) * (b `1)) by GROUP_1:def 3
.= ((((z `2) * ((a `1) * (b `1))) * (u `1)) * (v `1)) / ((a `1) * (b `1)) by A5, GROUP_1:def 3
.= ((((z `2) * (u `1)) * ((a `1) * (b `1))) * (v `1)) / ((a `1) * (b `1)) by GROUP_1:def 3
.= ((((z `2) * (u `1)) * (v `1)) * ((a `1) * (b `1))) / ((a `1) * (b `1)) by GROUP_1:def 3
.= (((z `2) * (u `1)) * (v `1)) * (((a `1) * (b `1)) / ((a `1) * (b `1))) by A18, A17, GCD_1:11
.= (((z `2) * (u `1)) * (v `1)) * (1_ I) by A18, GCD_1:9
.= ((z `2) * (u `1)) * (v `1)
.= (z `2) * ((u `1) * (v `1)) by GROUP_1:def 3 ;
hence z in QClass. (pmult (u,v)) by A1, Def4; :: thesis: verum
end;
end;
end;
hence z in QClass. (pmult (u,v)) ; :: thesis: verum
end;
for z being Element of Q. I st z in QClass. (pmult (u,v)) holds
z in qmult ((QClass. u),(QClass. v))
proof
let z be Element of Q. I; :: thesis: ( z in QClass. (pmult (u,v)) implies z in qmult ((QClass. u),(QClass. v)) )
assume z in QClass. (pmult (u,v)) ; :: thesis: z in qmult ((QClass. u),(QClass. v))
then A24: (z `1) * ((u `2) * (v `2)) = (z `2) * ((u `1) * (v `1)) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th5;
hence z in qmult ((QClass. u),(QClass. v)) by A24, Def7; :: thesis: verum
end;
hence qmult ((QClass. u),(QClass. v)) = QClass. (pmult (u,v)) by A2, SUBSET_1:3; :: thesis: verum