let x be Element of F_Complex; :: thesis: FQ_Ring x is Ring
reconsider ZS = doubleLoopStr(# (FQ x),(FQ_add x),(FQ_mult x),(In ((1. F_Complex),(FQ x))),(In ((0. F_Complex),(FQ x))) #) as non empty doubleLoopStr ;
A1: for v, w being Element of ZS holds v + w = w + v

proof

let v, w be Element of ZS; :: thesis: v + w = w + v
( v in F_Complex & w in F_Complex ) by Lm45;
then reconsider v1 = v, w1 = w as Element of F_Complex ;
thus v + w = w1 + v1 by Th49
.= w + v by Th49 ; :: thesis: verum

end;

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

proof

let u, v, w be Element of ZS; :: thesis: (u + v) + w = u + (v + w)
( u in F_Complex & v in F_Complex & w in F_Complex ) by Lm45;
then reconsider u1 = u, v1 = v, w1 = w as Element of F_Complex ;
A3: u + v = u1 + v1 by Th49;
A4: v + w = v1 + w1 by Th49;
thus (u + v) + w = (u1 + v1) + w1 by Th49, A3
.= u1 + (v1 + w1)
.= u + (v + w) by Th49, A4 ; :: thesis: verum

end;

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

proof

let v be Element of ZS; :: thesis: v + (0. ZS) = v
A6: 0. ZS = 0. F_Complex by Lm48, Lm7, SUBSET_1:def 8;
( 0. ZS in F_Complex & v in F_Complex ) by Lm45;
then reconsider v1 = v as Element of F_Complex ;
thus v + (0. ZS) = v1 + (0. F_Complex) by Th49, A6
.= v ; :: thesis: verum

end;

A7: for v being Element of ZS holds v is right_complementable

proof

let v be Element of ZS; :: thesis: v is right_complementable
v in F_Complex by Lm45;
then reconsider v1 = v as Element of F_Complex ;
A8: (- (1. F_Complex)) * v1 = - ((1. F_Complex) * v1) by VECTSP_1:9
.= - v1 ;
reconsider w1 = - (1. F_Complex) as Element of ZS by Lm48, Lm53;
A10: w1 * v = (- (1. F_Complex)) * v1 by Th50;
take w1 * v ; :: according to ALGSTR_0:def 11 :: thesis: v + (w1 * v) = 0. ZS
thus v + (w1 * v) = v1 + ((- (1. F_Complex)) * v1) by A10, Th49
.= 0. F_Complex by RLVECT_1:5, A8
.= 0. ZS by Lm48, Lm7, SUBSET_1:def 8 ; :: thesis: verum

end;

A11: for a, b, v being Element of ZS holds (a + b) * v = (a * v) + (b * v)

proof

let a, b, v be Element of ZS; :: thesis: (a + b) * v = (a * v) + (b * v)
( a in F_Complex & b in F_Complex & v in F_Complex ) by Lm45;
then reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex ;
A12: a + b in FQ x ;
reconsider ab = a + b as Element of F_Complex by A12;
A13: ( a1 * v1 = a * v & b1 * v1 = b * v ) by Th50;
thus (a + b) * v = ab * v1 by Th50
.= (a1 + b1) * v1 by Th49
.= (a1 * v1) + (b1 * v1)
.= (a * v) + (b * v) by A13, Th49 ; :: thesis: verum

end;

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

proof

let a, v, w be Element of ZS; :: thesis: ( a * (v + w) = (a * v) + (a * w) & (v + w) * a = (v * a) + (w * a) )
( a in F_Complex & v in F_Complex & w in F_Complex ) by Lm45;
then reconsider a1 = a, v1 = v, w1 = w as Element of F_Complex ;
A15: v + w in FQ x ;
reconsider vw = v + w as Element of F_Complex by A15;
A16: ( a1 * v1 = a * v & a1 * w1 = a * w ) by Th50;
thus a * (v + w) = a1 * vw by Th50
.= a1 * (v1 + w1) by Th49
.= (a1 * v1) + (a1 * w1)
.= (a * v) + (a * w) by A16, Th49 ; :: thesis: (v + w) * a = (v * a) + (w * a)
thus (v + w) * a = (v * a) + (w * a) by A11; :: thesis: verum

end;

A17: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)

proof

let a, b, v be Element of ZS; :: thesis: (a * b) * v = a * (b * v)
( a in F_Complex & b in F_Complex & v in F_Complex ) by Lm45;
then reconsider a1 = a, b1 = b, v1 = v as Element of F_Complex ;
A18: ( a * b in FQ x & b * v in FQ x ) ;
reconsider ab = a * b, bv = b * v as Element of F_Complex by A18;
thus (a * b) * v = ab * v1 by Th50
.= (a1 * b1) * v1 by Th50
.= a1 * (b1 * v1)
.= a1 * bv by Th50
.= a * (b * v) by Th50 ; :: thesis: verum

end;

for v being Element of ZS holds
( v * (1. ZS) = v & (1. ZS) * v = v )

proof

let v be Element of ZS; :: thesis: ( v * (1. ZS) = v & (1. ZS) * v = v )
A19: 1. ZS = 1. F_Complex by Lm52;
v in F_Complex by Lm45;
then reconsider v1 = v as Element of F_Complex ;
thus v * (1. ZS) = v1 * (1. F_Complex) by A19, Th50
.= v ; :: thesis: (1. ZS) * v = v
thus (1. ZS) * v = (1. F_Complex) * v1 by A19, Th50
.= v ; :: thesis: verum

end;

hence FQ_Ring x is Ring by A1, A2, A5, A7, A14, A17, VECTSP_1:def 6, VECTSP_1:def 7, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, ALGSTR_0:def 16; :: thesis: verum