set ccs = NonZero R;
set cR = the carrier of R;
reconsider ccs = NonZero R as non empty set ;
set mcs = the multF of R || ccs;
[:ccs,ccs:] c= [: the carrier of R, the carrier of R:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:ccs,ccs:] or x in [: the carrier of R, the carrier of R:] )
assume x in [:ccs,ccs:] ; :: thesis: x in [: the carrier of R, the carrier of R:]
then ex a, b being object st
( a in ccs & b in ccs & x = [a,b] ) by ZFMISC_1:def 2;
hence x in [: the carrier of R, the carrier of R:] by ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider mcs = the multF of R || ccs as Function of [:ccs,ccs:], the carrier of R by FUNCT_2:32;
rng mcs c= ccs
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng mcs or y in ccs )
assume y in rng mcs ; :: thesis: y in ccs
then consider x being object such that
A1: x in dom mcs and
A2: y = mcs . x by FUNCT_1:def 3;
A3: dom mcs = [:ccs,ccs:] by FUNCT_2:def 1;
then consider a, b being object such that
A4: a in ccs and
A5: b in ccs and
A6: x = [a,b] by A1, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of the carrier of R by A4, A5;
not b in {(0. R)} by A5, XBOOLE_0:def 5;
then A7: b <> 0. R by TARSKI:def 1;
not a in {(0. R)} by A4, XBOOLE_0:def 5;
then a <> 0. R by TARSKI:def 1;
then a * b <> 0. R by A7, VECTSP_2:12;
then A8: not a * b in {(0. R)} by TARSKI:def 1;
mcs . x = a * b by A1, A3, A6, FUNCT_1:49;
hence y in ccs by A2, A8, XBOOLE_0:def 5; :: thesis: verum
end;
then reconsider mcs = mcs as BinOp of ccs by FUNCT_2:6;
reconsider cs = multMagma(# ccs,mcs #) as non empty multMagma ;
set ccs1 = the carrier of cs;
A9: now :: thesis: for a, b being Element of the carrier of R
for c, d being Element of the carrier of cs st a = c & b = d holds
a * b = c * d
let a, b be Element of the carrier of R; :: thesis: for c, d being Element of the carrier of cs st a = c & b = d holds
a * b = c * d
let c, d be Element of the carrier of cs; :: thesis: ( a = c & b = d implies a * b = c * d )
assume A10: ( a = c & b = d ) ; :: thesis: a * b = c * d
[c,d] in [:ccs,ccs:] by ZFMISC_1:def 2;
hence a * b = c * d by A10, FUNCT_1:49; :: thesis: verum
end;
A11: not 1_ R in {(0. R)} by TARSKI:def 1;
A12: cs is Group-like
proof
reconsider e = 1_ R as Element of the carrier of cs by A11, XBOOLE_0:def 5;
take e ; :: according to GROUP_1:def 2 :: thesis: for b1 being Element of the carrier of cs holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of cs st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of the carrier of cs; :: thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of cs st
( h * b1 = e & b1 * h = e ) )
h in ccs ;
then reconsider h9 = h as Scalar of R ;
thus h * e = h9 * (1_ R) by A9
.= h ; :: thesis: ( e * h = h & ex b1 being Element of the carrier of cs st
( h * b1 = e & b1 * h = e ) )
thus e * h = (1_ R) * h9 by A9
.= h ; :: thesis: ex b1 being Element of the carrier of cs st
( h * b1 = e & b1 * h = e )
not h in {(0. R)} by XBOOLE_0:def 5;
then A13: h <> 0. R by TARSKI:def 1;
then h9 " <> 0. R by VECTSP_2:13;
then not h9 " in {(0. R)} by TARSKI:def 1;
then reconsider g = h9 " as Element of the carrier of cs by XBOOLE_0:def 5;
take g ; :: thesis: ( h * g = e & g * h = e )
thus h * g = h9 * (h9 ") by A9
.= e by A13, VECTSP_2:9 ; :: thesis: g * h = e
thus g * h = (h9 ") * h9 by A9
.= e by A13, VECTSP_2:9 ; :: thesis: verum
end;
cs is associative
proof
let x, y, z be Element of the carrier of cs; :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
A14: z in the carrier of cs ;
( x in the carrier of cs & y in the carrier of cs ) ;
then reconsider x9 = x, y9 = y, z9 = z as Element of the carrier of R by A14;
A15: y9 * z9 = y * z by A9;
x9 * y9 = x * y by A9;
hence (x * y) * z = (x9 * y9) * z9 by A9
.= x9 * (y9 * z9) by GROUP_1:def 3
.= x * (y * z) by A9, A15 ;
:: thesis: verum
end;
hence ex b1 being strict Group st
( the carrier of b1 = NonZero R & the multF of b1 = the multF of R || the carrier of b1 ) by A12; :: thesis: verum