A1: ( ( 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

set d = (r1 * s1) / (gcd s1,r2,Amp);
assume that
A2: ( r1 = 0. R or s1 = 0. R ) and
A3: r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) )
A4: gcd s1,r2,Amp <> 0. R by A3, Th34;
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) )
A5: r1 * s1 = 0. R

proof

now

per cases ( r1 = 0. R or s1 = 0. R ) by A2;

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 gcd s1,r2,Amp divides r1 * s1 by Th7;
then ((r1 * s1) / (gcd s1,r2,Amp)) * (gcd s1,r2,Amp) = 0. R by A5, A4, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd s1,r2,Amp) ) by A4, VECTSP_2:def 5; :: thesis: verum

end;

A6: ( 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 that
s2 <> 0. R and
A7: r2 = 1. R and
r2 <> 0. R and
A8: 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) )
gcd s1,r2,Amp = 1. R by A7, 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 A8, Th33; :: thesis: verum

end;

A9: ( ( 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

set d = (r1 * s1) / (gcd r1,s2,Amp);
assume that
A10: ( r1 = 0. R or s1 = 0. R ) and
A11: s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) )
A12: gcd r1,s2,Amp <> 0. R by A11, Th34;
let z be Element of R; :: thesis: ( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) )
A13: r1 * s1 = 0. R

proof

now

per cases ( r1 = 0. R or s1 = 0. R ) by A10;

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 gcd r1,s2,Amp divides r1 * s1 by Th7;
then ((r1 * s1) / (gcd r1,s2,Amp)) * (gcd r1,s2,Amp) = 0. R by A13, A12, Def4;
hence ( z = 0. R iff z = (r1 * s1) / (gcd r1,s2,Amp) ) by A12, VECTSP_2:def 5; :: 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 that
A15: r2 = 1. R and
s2 = 1. R and
r2 <> 0. R and
s2 = 1. R ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd s1,r2,Amp) )
gcd s1,r2,Amp = 1. R by A15, 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;

A16: ( ( 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 that
A17: ( r1 = 0. R or s1 = 0. R ) and
r2 = 1. R and
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 A17;

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;

( 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 that
r2 = 1. R and
A18: s2 = 1. R and
s2 <> 0. R and
r2 = 1. R ; :: thesis: for z being Element of R holds
( z = r1 * s1 iff z = (r1 * s1) / (gcd r1,s2,Amp) )
gcd r1,s2,Amp = 1. R by A18, 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;

hence for b₁ being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b₁ = 0. R iff b₁ = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = r1 * s1 iff b₁ = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b₁ = (r1 * s1) / (gcd r1,s2,Amp) iff b₁ = (r1 * s1) / (gcd s1,r2,Amp) ) ) ) by A16, A9, A1, A14, A6; :: thesis: verum