A1: ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies for z being Element of R holds
( z = 0. R iff z = r1 * s1 ) )
proof
assume A2: ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = 0. R iff z = r1 * s1 )
now
per cases ( r1 = 0. R or s1 = 0. R ) by A2;
case r1 = 0. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = r1 * s1 )
hence for z being Element of R holds
( z = 0. R iff z = r1 * s1 ) by VECTSP_1:39; :: thesis: verum
end;
case s1 = 0. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = r1 * s1 )
hence for z being Element of R holds
( z = 0. R iff z = r1 * s1 ) by VECTSP_1:39; :: thesis: verum
end;
end;
end;
hence for z being Element of R holds
( z = 0. R iff z = r1 * s1 ) ; :: thesis: verum
end;
A3: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) ) )
proof
assume A4: ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) )
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) )
A5: r1 * s1 = 0. R
proof
now
per cases ( r1 = 0. R or s1 = 0. R ) by A4;
case r1 = 0. R ; :: thesis: r1 * s1 = 0. R
hence r1 * s1 = 0. R by VECTSP_1:39; :: thesis: verum
end;
case s1 = 0. R ; :: thesis: r1 * s1 = 0. R
hence r1 * s1 = 0. R by VECTSP_1:39; :: thesis: verum
end;
end;
end;
hence r1 * s1 = 0. R ; :: thesis: verum
end;
gcd r1,s2,Amp divides r1 by Def12;
then A6: gcd r1,s2,Amp divides r1 * s1 by Th7;
A7: gcd r1,s2,Amp <> 0. R by A4, Th34;
set d = (r1 * s1) / (gcd r1,s2,Amp);
((r1 * s1) / (gcd r1,s2,Amp)) * (gcd r1,s2,Amp) = 0. R by A5, A6, A7, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) ) by A7, VECTSP_2:def 5; :: thesis: verum
end;
A8: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) ) )
proof
assume A9: ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) )
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) )
A10: r1 * s1 = 0. R
proof
now
per cases ( r1 = 0. R or s1 = 0. R ) by A9;
case r1 = 0. R ; :: thesis: r1 * s1 = 0. R
hence r1 * s1 = 0. R by VECTSP_1:39; :: thesis: verum
end;
case s1 = 0. R ; :: thesis: r1 * s1 = 0. R
hence r1 * s1 = 0. R by VECTSP_1:39; :: thesis: verum
end;
end;
end;
hence r1 * s1 = 0. R ; :: thesis: verum
end;
gcd s1,r2,Amp divides s1 by Def12;
then A11: gcd s1,r2,Amp divides r1 * s1 by Th7;
A12: gcd s1,r2,Amp <> 0. R by A9, Th34;
set d = (r1 * s1) / (gcd s1,r2,Amp);
((r1 * s1) / (gcd s1,r2,Amp)) * (gcd s1,r2,Amp) = 0. R by A10, A11, A12, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) ) by A12, VECTSP_2:def 5; :: thesis: verum
end;
A13: ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd r1,s2,Amp) ) )
proof
assume ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd r1,s2,Amp) )
then gcd r1,s2,Amp = 1. R by Th33;
hence for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd r1,s2,Amp) ) by Th10; :: thesis: verum
end;
A14: ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd s1,r2,Amp) ) )
proof
assume ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd s1,r2,Amp) )
then gcd s1,r2,Amp = 1. R by Th33;
hence for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd s1,r2,Amp) ) by Th10; :: thesis: verum
end;
( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies for z being Element of R holds
( z = (r1 * s1) / (gcd r1,s2,Amp) iff z = (r1 * s1) / (gcd s1,r2,Amp) ) )
proof
assume A15: ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R ) ; :: thesis: for z being Element of R holds
( z = (r1 * s1) / (gcd r1,s2,Amp) iff z = (r1 * s1) / (gcd s1,r2,Amp) )
then gcd s1,r2,Amp = 1. R by Th33;
hence for z being Element of R holds
( z = (r1 * s1) / (gcd r1,s2,Amp) iff z = (r1 * s1) / (gcd s1,r2,Amp) ) by A15, Th33; :: thesis: verum
end;
hence for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 0. R iff b1 = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = (r1 * s1) / (gcd r1,s2,Amp) iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) ) by A1, A3, A8, A13, A14; :: thesis: verum