let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of Quot. I holds
( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u )
let u be Element of Quot. I; :: thesis: ( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u )
consider x being Element of Q. I such that
A1: q0. I = QClass. x by Def5;
consider y being Element of Q. I such that
A2: u = QClass. y by Def5;
A3: x `2 <> 0. I by Th2;
y `2 <> 0. I by Th2;
then (x `2) * (y `2) <> 0. I by A3, VECTSP_2:def 1;
then reconsider t = [(((y `1) * (x `2)) + ((x `1) * (y `2))),((x `2) * (y `2))] as Element of Q. I by Def1;
x in q0. I by A1, Th5;
then A4: x `1 = 0. I by Def8;
A5: for z being Element of Q. I st z in QClass. y holds
z in QClass. t
proof
let z be Element of Q. I; :: thesis: ( z in QClass. y implies z in QClass. t )
assume z in QClass. y ; :: thesis: z in QClass. t
then A6: (z `1) * (y `2) = (z `2) * (y `1) by Def4;
(z `1) * (t `2) = (z `1) * ((x `2) * (y `2))
.= ((z `2) * (y `1)) * (x `2) by A6, GROUP_1:def 3
.= (z `2) * ((y `1) * (x `2)) by GROUP_1:def 3
.= (z `2) * (((y `1) * (x `2)) + (0. I)) by RLVECT_1:4
.= (z `2) * (((y `1) * (x `2)) + ((x `1) * (y `2))) by A4
.= (z `2) * (t `1) ;
hence z in QClass. t by Def4; :: thesis: verum
end;
A7: for z being Element of Q. I st z in QClass. t holds
z in QClass. y
proof
let z be Element of Q. I; :: thesis: ( z in QClass. t implies z in QClass. y )
x `2 divides x `2 ;
then A8: x `2 divides ((z `1) * (y `2)) * (x `2) by GCD_1:7;
x `2 divides x `2 ;
then A9: x `2 divides ((z `2) * (y `1)) * (x `2) by GCD_1:7;
assume z in QClass. t ; :: thesis: z in QClass. y
then (z `1) * (t `2) = (z `2) * (t `1) by Def4;
then A10: (z `1) * ((x `2) * (y `2)) = (z `2) * (t `1) ;
A11: ((z `1) * (y `2)) * (x `2) = (z `1) * ((x `2) * (y `2)) by GROUP_1:def 3
.= (z `2) * (((y `1) * (x `2)) + ((0. I) * (y `2))) by A4, A10
.= (z `2) * (((y `1) * (x `2)) + (0. I))
.= (z `2) * ((y `1) * (x `2)) by RLVECT_1:4
.= ((z `2) * (y `1)) * (x `2) by GROUP_1:def 3 ;
(z `1) * (y `2) = ((z `1) * (y `2)) * (1_ I)
.= ((z `1) * (y `2)) * ((x `2) / (x `2)) by A3, GCD_1:9
.= (((z `2) * (y `1)) * (x `2)) / (x `2) by A3, A11, A8, GCD_1:11
.= ((z `2) * (y `1)) * ((x `2) / (x `2)) by A3, A9, GCD_1:11
.= ((z `2) * (y `1)) * (1_ I) by A3, GCD_1:9
.= (z `2) * (y `1) ;
hence z in QClass. y by Def4; :: thesis: verum
end;
( qadd (u,(q0. I)) = QClass. (padd (y,x)) & qadd ((q0. I),u) = QClass. (padd (x,y)) ) by A1, A2, Th9;
hence ( qadd (u,(q0. I)) = u & qadd ((q0. I),u) = u ) by A2, A5, A7, SUBSET_1:3; :: thesis: verum