let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of Q. I holds qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v))
let u, v be Element of Q. I; :: thesis: qadd ((QClass. u),(QClass. v)) = QClass. (padd (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 `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
A1: ( w `1 = ((u `1) * (v `2)) + ((v `1) * (u `2)) & w `2 = (u `2) * (v `2) ) ;
A2: for z being Element of Q. I st z in qadd ((QClass. u),(QClass. v)) holds
z in QClass. (padd (u,v))
proof
let z be Element of Q. I; :: thesis: ( z in qadd ((QClass. u),(QClass. v)) implies z in QClass. (padd (u,v)) )
assume z in qadd ((QClass. u),(QClass. v)) ; :: thesis: z in QClass. (padd (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 `2)) + ((b `1) * (a `2))) by Def6;
A6: (a `1) * (u `2) = (a `2) * (u `1) by A3, Def4;
A7: (b `1) * (v `2) = (b `2) * (v `1) by A4, Def4;
(a `2) * (b `2) divides (a `2) * (b `2) ;
then A8: (a `2) * (b `2) divides ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((a `2) * (b `2)) by GCD_1:7;
A9: (a `2) * (b `2) divides (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) by A5, GCD_1:def 1;
then A10: (a `2) * (b `2) divides ((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) * ((u `2) * (v `2)) by GCD_1:7;
( a `2 <> 0. I & b `2 <> 0. I ) by Th2;
then A11: (a `2) * (b `2) <> 0. I by VECTSP_2:def 1;
then z `1 = ((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) / ((a `2) * (b `2)) by A5, A9, GCD_1:def 4;
then (z `1) * ((u `2) * (v `2)) = (((z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2)))) * ((u `2) * (v `2))) / ((a `2) * (b `2)) by A11, A9, A10, GCD_1:11
.= ((z `2) * ((((a `1) * (b `2)) + ((b `1) * (a `2))) * ((u `2) * (v `2)))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((a `1) * (b `2)) * ((u `2) * (v `2))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by VECTSP_1:def 3
.= ((z `2) * (((b `2) * ((a `1) * ((u `2) * (v `2)))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + (((b `1) * (a `2)) * ((u `2) * (v `2))))) / ((a `2) * (b `2)) by A6, GROUP_1:def 3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + ((a `2) * ((b `1) * ((v `2) * (u `2)))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * (((b `2) * (((a `2) * (u `1)) * (v `2))) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by A7, GROUP_1:def 3
.= ((z `2) * ((((b `2) * ((a `2) * (u `1))) * (v `2)) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * ((b `2) * (a `2))) * (v `2)) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * (v `2)) * ((b `2) * (a `2))) + ((a `2) * (((b `2) * (v `1)) * (u `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * (v `2)) * ((b `2) * (a `2))) + (((a `2) * ((b `2) * (v `1))) * (u `2)))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * (v `2)) * ((a `2) * (b `2))) + (((v `1) * ((a `2) * (b `2))) * (u `2)))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * (v `2)) * ((a `2) * (b `2))) + (((v `1) * (u `2)) * ((a `2) * (b `2))))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * ((((u `1) * (v `2)) + ((v `1) * (u `2))) * ((a `2) * (b `2)))) / ((a `2) * (b `2)) by VECTSP_1:def 3
.= (((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((a `2) * (b `2))) / ((a `2) * (b `2)) by GROUP_1:def 3
.= ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * (((a `2) * (b `2)) / ((a `2) * (b `2))) by A11, A8, GCD_1:11
.= ((z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2)))) * (1_ I) by A11, GCD_1:9
.= (z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2))) ;
hence z in QClass. (padd (u,v)) by A1, Def4; :: thesis: verum
end;
for z being Element of Q. I st z in QClass. (padd (u,v)) holds
z in qadd ((QClass. u),(QClass. v))
proof
let z be Element of Q. I; :: thesis: ( z in QClass. (padd (u,v)) implies z in qadd ((QClass. u),(QClass. v)) )
assume z in QClass. (padd (u,v)) ; :: thesis: z in qadd ((QClass. u),(QClass. v))
then A12: (z `1) * ((u `2) * (v `2)) = (z `2) * (((u `1) * (v `2)) + ((v `1) * (u `2))) by A1, Def4;
( u in QClass. u & v in QClass. v ) by Th5;
hence z in qadd ((QClass. u),(QClass. v)) by A12, Def6; :: thesis: verum
end;
hence qadd ((QClass. u),(QClass. v)) = QClass. (padd (u,v)) by A2, SUBSET_1:3; :: thesis: verum