set ZS = Gauss_RAT_Ring ;
A1: for v, w being Element of Gauss_RAT_Ring holds v + w = w + v

proof

let v, w be Element of Gauss_RAT_Ring; :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as G_RAT by Th10;
thus v + w = v1 + w1 by Th27
.= w + v by Th27 ; :: thesis: verum

end;

A2: for u, v, w being Element of Gauss_RAT_Ring holds (u + v) + w = u + (v + w)

proof

let u, v, w be Element of Gauss_RAT_Ring; :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as G_RAT by Th10;
A3: u + v = u1 + v1 by Th27;
A4: v + w = v1 + w1 by Th27;
thus (u + v) + w = (u1 + v1) + w1 by Th27, A3
.= u1 + (v1 + w1)
.= u + (v + w) by Th27, A4 ; :: thesis: verum

end;

A5: for v being Element of Gauss_RAT_Ring holds v + (0. Gauss_RAT_Ring) = v

proof

let v be Element of Gauss_RAT_Ring; :: thesis: v + (0. Gauss_RAT_Ring) = v
reconsider v1 = v as G_RAT by Th10;
thus v + (0. Gauss_RAT_Ring) = v1 + 0 by Th27
.= v ; :: thesis: verum

end;

A6: for v being Element of Gauss_RAT_Ring holds v is right_complementable

proof

let v be Element of Gauss_RAT_Ring; :: thesis: v is right_complementable
reconsider v1 = v as G_RAT by Th10;
reconsider w1 = - 1 as Element of Gauss_RAT_Ring by Th11;
A7: w1 * v = (- 1) * v1 by Th29;
take w1 * v ; :: according to ALGSTR_0:def 11 :: thesis: v + (w1 * v) = 0. Gauss_RAT_Ring
thus v + (w1 * v) = v1 + ((- 1) * v1) by A7, Th27
.= 0. Gauss_RAT_Ring ; :: thesis: verum

end;

A8: for a, b, v being Element of Gauss_RAT_Ring holds (a + b) * v = (a * v) + (b * v)

proof

let a, b, v be Element of Gauss_RAT_Ring; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_RAT by Th10;
reconsider ab = a + b as G_RAT by Th10;
A9: ( a1 * v1 = a * v & b1 * v1 = b * v ) by Th29;
thus (a + b) * v = ab * v1 by Th29
.= (a1 + b1) * v1 by Th27
.= (a1 * v1) + (b1 * v1)
.= (a * v) + (b * v) by A9, Th27 ; :: thesis: verum

end;

A10: for a, v, w being Element of Gauss_RAT_Ring holds
( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )

proof

let a, v, w be Element of Gauss_RAT_Ring; :: thesis: ( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )
reconsider a1 = a, v1 = v, w1 = w as G_RAT by Th10;
reconsider vw = v + w as G_RAT by Th10;
A11: ( a1 * v1 = a * v & a1 * w1 = a * w ) by Th29;
thus a * (v + w) = a1 * vw by Th29
.= a1 * (v1 + w1) by Th27
.= (a1 * v1) + (a1 * w1)
.= (a * v) + (a * w) by A11, Th27 ; :: thesis: (v + w) * a = (v * a) + (w * a)
thus (v + w) * a = (v * a) + (w * a) by A8; :: thesis: verum

end;

A12: for a, b being Element of Gauss_RAT_Ring holds a * b = b * a

proof

let a, b be Element of Gauss_RAT_Ring; :: thesis: a * b = b * a
reconsider a1 = a, b1 = b as G_RAT by Th10;
thus a * b = a1 * b1 by Th29
.= b * a by Th29 ; :: thesis: verum

end;

A13: for a, b, v being Element of Gauss_RAT_Ring holds (a * b) * v = a * (b * v)

proof

let a, b, v be Element of Gauss_RAT_Ring; :: thesis: (a * b) * v = a * (b * v)
reconsider a1 = a, b1 = b, v1 = v as G_RAT by Th10;
reconsider ab = a * b, bv = b * v as G_RAT by Th10;
thus (a * b) * v = ab * v1 by Th29
.= (a1 * b1) * v1 by Th29
.= a1 * (b1 * v1)
.= a1 * bv by Th29
.= a * (b * v) by Th29 ; :: thesis: verum

end;

A14: for v being Element of Gauss_RAT_Ring holds
( v * (1. Gauss_RAT_Ring) = v & (1. Gauss_RAT_Ring) * v = v )

proof

let v be Element of Gauss_RAT_Ring; :: thesis: ( v * (1. Gauss_RAT_Ring) = v & (1. Gauss_RAT_Ring) * v = v )
reconsider v1 = v as G_RAT by Th10;
thus v * (1. Gauss_RAT_Ring) = v1 * 1 by Th29
.= v ; :: thesis: (1. Gauss_RAT_Ring) * v = v
thus (1. Gauss_RAT_Ring) * v = 1 * v1 by Th29
.= v ; :: thesis: verum

end;

for v being Element of Gauss_RAT_Ring st v <> 0. Gauss_RAT_Ring holds
v is left_invertible

proof

let v be Element of Gauss_RAT_Ring; :: thesis: ( v <> 0. Gauss_RAT_Ring implies v is left_invertible )
assume A15: v <> 0. Gauss_RAT_Ring ; :: thesis: v is left_invertible
reconsider v1 = v as G_RAT by Th10;
reconsider w = v1 " as Element of Gauss_RAT_Ring by Th11;
w * v = (v1 ") * v1 by Th29
.= 1. Gauss_RAT_Ring by A15, XCMPLX_0:def 7 ;
hence v is left_invertible ; :: thesis: verum

end;

hence Gauss_RAT_Ring is Field by A1, A2, A5, A6, A10, A13, A14, A12, VECTSP_1:def 6, VECTSP_1:def 7, ALGSTR_0:def 39, GROUP_1:def 3, GROUP_1:def 12, STRUCT_0:def 8, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; :: thesis: verum