let K be Skew-Field; :: thesis: opp K is Skew-Field

set L = opp K;

for x being Scalar of (opp K) holds

( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )

set L = opp K;

for x being Scalar of (opp K) holds

( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )

proof

hence
opp K is Skew-Field
by STRUCT_0:def 8, VECTSP_1:def 9; :: thesis: verum
let x be Scalar of (opp K); :: thesis: ( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )

( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) )

end;( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) )

proof

hence
( ( x <> 0. (opp K) implies ex y being Scalar of (opp K) st y * x = 1_ (opp K) ) & 0. (opp K) <> 1_ (opp K) )
; :: thesis: verum
reconsider a = x as Scalar of K ;

assume x <> 0. (opp K) ; :: thesis: ex y being Scalar of (opp K) st y * x = 1_ (opp K)

then consider b being Scalar of K such that

A1: a * b = 1_ K by VECTSP_2:6;

reconsider y = b as Scalar of (opp K) ;

take y ; :: thesis: y * x = 1_ (opp K)

thus y * x = 1_ (opp K) by A1, Lm3; :: thesis: verum

end;assume x <> 0. (opp K) ; :: thesis: ex y being Scalar of (opp K) st y * x = 1_ (opp K)

then consider b being Scalar of K such that

A1: a * b = 1_ K by VECTSP_2:6;

reconsider y = b as Scalar of (opp K) ;

take y ; :: thesis: y * x = 1_ (opp K)

thus y * x = 1_ (opp K) by A1, Lm3; :: thesis: verum