thus for P, Q being Element of ProjCo (GF p) st ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) holds
ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) :: thesis: verum
proof
let P, Q be Element of ProjCo (GF p); :: thesis: ( ex a being Element of (GF p) st
( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) implies ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) )
given a being Element of (GF p) such that A1: ( a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) ) ; :: thesis: ex b being Element of (GF p) st
( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) )
take b = a " ; :: thesis: ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) )
A2: b <> 0. (GF p)
proof
assume b = 0. (GF p) ; :: thesis: contradiction
then b * a = 0. (GF p) ;
then 1. (GF p) = 0. (GF p) by A1, VECTSP_1:def 10;
hence contradiction ; :: thesis: verum
end;
A3: Q `1_3 = (1. (GF p)) * (Q `1_3)
.= (b * a) * (Q `1_3) by A1, VECTSP_1:def 10
.= b * (P `1_3) by A1, GROUP_1:def 3 ;
A4: Q `2_3 = (1. (GF p)) * (Q `2_3)
.= (b * a) * (Q `2_3) by A1, VECTSP_1:def 10
.= b * (P `2_3) by A1, GROUP_1:def 3 ;
Q `3_3 = (1. (GF p)) * (Q `3_3)
.= (b * a) * (Q `3_3) by A1, VECTSP_1:def 10
.= b * (P `3_3) by A1, GROUP_1:def 3 ;
hence ( b <> 0. (GF p) & Q `1_3 = b * (P `1_3) & Q `2_3 = b * (P `2_3) & Q `3_3 = b * (P `3_3) ) by A2, A3, A4; :: thesis: verum
end;