let Q be multLoop; :: thesis: for f being Function of Q,Q st f in Mlt (Nucl Q) holds
ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = u * (x * v) ) )
set H = Nucl Q;
defpred S3[ Function of Q,Q] means ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds $1 . x = u * (x * v) ) );
A1: for u being Element of Q st u in Nucl Q holds
for f being Function of Q,Q st ( for x being Element of Q holds f . x = x * u ) holds
S3[f]
proof
let u be Element of Q; :: thesis: ( u in Nucl Q implies for f being Function of Q,Q st ( for x being Element of Q holds f . x = x * u ) holds
S3[f] )
assume A2: u in Nucl Q ; :: thesis: for f being Function of Q,Q st ( for x being Element of Q holds f . x = x * u ) holds
S3[f]
let f be Function of Q,Q; :: thesis: ( ( for x being Element of Q holds f . x = x * u ) implies S3[f] )
assume A3: for x being Element of Q holds f . x = x * u ; :: thesis: S3[f]
take 1. Q ; :: thesis: ex v being Element of Q st
( 1. Q in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = (1. Q) * (x * v) ) )
take u ; :: thesis: ( 1. Q in Nucl Q & u in Nucl Q & ( for x being Element of Q holds f . x = (1. Q) * (x * u) ) )
thus ( 1. Q in Nucl Q & u in Nucl Q & ( for x being Element of Q holds f . x = (1. Q) * (x * u) ) ) by A3, A2, Th20; :: thesis: verum
end;
A4: for u being Element of Q st u in Nucl Q holds
for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f]
proof
let u be Element of Q; :: thesis: ( u in Nucl Q implies for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f] )
assume A5: u in Nucl Q ; :: thesis: for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f]
let f be Function of Q,Q; :: thesis: ( ( for x being Element of Q holds f . x = u * x ) implies S3[f] )
assume A6: for x being Element of Q holds f . x = u * x ; :: thesis: S3[f]
take u ; :: thesis: ex v being Element of Q st
( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = u * (x * v) ) )
take 1. Q ; :: thesis: ( u in Nucl Q & 1. Q in Nucl Q & ( for x being Element of Q holds f . x = u * (x * (1. Q)) ) )
thus ( u in Nucl Q & 1. Q in Nucl Q & ( for x being Element of Q holds f . x = u * (x * (1. Q)) ) ) by A6, A5, Th20; :: thesis: verum
end;
A7: for g, h being Permutation of the carrier of Q st S3[g] & S3[h] holds
S3[g * h]
proof
let g, h be Permutation of the carrier of Q; :: thesis: ( S3[g] & S3[h] implies S3[g * h] )
assume A8: ( S3[g] & S3[h] ) ; :: thesis: S3[g * h]
consider u, v being Element of Q such that
A9: ( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds g . x = u * (x * v) ) ) by A8;
consider z, w being Element of Q such that
A10: ( z in Nucl Q & w in Nucl Q & ( for x being Element of Q holds h . x = z * (x * w) ) ) by A8;
take u * z ; :: thesis: ex v being Element of Q st
( u * z in Nucl Q & v in Nucl Q & ( for x being Element of Q holds (g * h) . x = (u * z) * (x * v) ) )
take w * v ; :: thesis: ( u * z in Nucl Q & w * v in Nucl Q & ( for x being Element of Q holds (g * h) . x = (u * z) * (x * (w * v)) ) )
( u in [#] (lp (Nucl Q)) & z in [#] (lp (Nucl Q)) ) by Th24, A9, A10;
then u * z in [#] (lp (Nucl Q)) by Th37;
hence u * z in Nucl Q by Th24; :: thesis: ( w * v in Nucl Q & ( for x being Element of Q holds (g * h) . x = (u * z) * (x * (w * v)) ) )
( w in [#] (lp (Nucl Q)) & v in [#] (lp (Nucl Q)) ) by Th24, A9, A10;
then A11: w * v in [#] (lp (Nucl Q)) by Th37;
then A12: w * v in Nucl Q by Th24;
thus w * v in Nucl Q by A11, Th24; :: thesis: for x being Element of Q holds (g * h) . x = (u * z) * (x * (w * v))
A13: u in Nucl_l Q by A9, Th12;
A14: v in Nucl_r Q by A9, Th12;
A15: w in Nucl_r Q by A10, Th12;
A16: w * v in Nucl_r Q by A12, Th12;
let x be Element of Q; :: thesis: (g * h) . x = (u * z) * (x * (w * v))
(g * h) . x = g . (h . x) by FUNCT_2:15
.= g . (z * (x * w)) by A10
.= u * ((z * (x * w)) * v) by A9
.= (u * (z * (x * w))) * v by A13, Def22
.= ((u * z) * (x * w)) * v by A13, Def22
.= (((u * z) * x) * w) * v by A15, Def24
.= ((u * z) * x) * (w * v) by A14, Def24
.= (u * z) * (x * (w * v)) by A16, Def24 ;
hence (g * h) . x = (u * z) * (x * (w * v)) ; :: thesis: verum
end;
A17: for g being Permutation of Q st S3[g] holds
S3[g " ]
proof
let g be Permutation of Q; :: thesis: ( S3[g] implies S3[g " ] )
assume S3[g] ; :: thesis: S3[g " ]
then consider u, v being Element of Q such that
A18: ( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds g . x = u * (x * v) ) ) ;
A19: u in Nucl_m Q by A18, Th12;
A20: ( v in Nucl_m Q & v in Nucl_r Q ) by A18, Th12;
take (1. Q) / u ; :: thesis: ex v being Element of Q st
( (1. Q) / u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds (g ") . x = ((1. Q) / u) * (x * v) ) )
take v \ (1. Q) ; :: thesis: ( (1. Q) / u in Nucl Q & v \ (1. Q) in Nucl Q & ( for x being Element of Q holds (g ") . x = ((1. Q) / u) * (x * (v \ (1. Q))) ) )
1. Q in Nucl Q by Th20;
then A21: 1. Q in [#] (lp (Nucl Q)) by Th24;
u in [#] (lp (Nucl Q)) by Th24, A18;
then (1. Q) / u in [#] (lp (Nucl Q)) by Th41, A21;
hence (1. Q) / u in Nucl Q by Th24; :: thesis: ( v \ (1. Q) in Nucl Q & ( for x being Element of Q holds (g ") . x = ((1. Q) / u) * (x * (v \ (1. Q))) ) )
v in [#] (lp (Nucl Q)) by Th24, A18;
then v \ (1. Q) in [#] (lp (Nucl Q)) by Th39, A21;
hence v \ (1. Q) in Nucl Q by Th24; :: thesis: for x being Element of Q holds (g ") . x = ((1. Q) / u) * (x * (v \ (1. Q)))
let x be Element of Q; :: thesis: (g ") . x = ((1. Q) / u) * (x * (v \ (1. Q)))
reconsider k = (curry the multF of Q) . ((1. Q) / u) as Permutation of Q by Th30;
reconsider h = (curry' the multF of Q) . (v \ (1. Q)) as Permutation of Q by Th31;
(k * h) * g = id Q
proof
for y being Element of Q holds ((k * h) * g) . y = (id Q) . y
proof
let y be Element of Q; :: thesis: ((k * h) * g) . y = (id Q) . y
((k * h) * g) . y = (k * h) . (g . y) by FUNCT_2:15
.= (k * h) . (u * (y * v)) by A18
.= k . (h . (u * (y * v))) by FUNCT_2:15
.= k . ((u * (y * v)) * (v \ (1. Q))) by FUNCT_5:70
.= k . (((u * y) * v) * (v \ (1. Q))) by Def24, A20
.= k . ((u * y) * (v * (v \ (1. Q)))) by Def23, A20
.= ((1. Q) / u) * (u * y) by FUNCT_5:69
.= (((1. Q) / u) * u) * y by Def23, A19
.= y ;
hence ((k * h) * g) . y = (id Q) . y ; :: thesis: verum
end;
hence (k * h) * g = id Q by FUNCT_2:def 8; :: thesis: verum
end;
then (g ") . x = (k * h) . x by FUNCT_2:60
.= k . (h . x) by FUNCT_2:15
.= k . (x * (v \ (1. Q))) by FUNCT_5:70
.= ((1. Q) / u) * (x * (v \ (1. Q))) by FUNCT_5:69 ;
hence (g ") . x = ((1. Q) / u) * (x * (v \ (1. Q))) ; :: thesis: verum
end;
for f being Function of Q,Q st f in Mlt (Nucl Q) holds
S3[f] from AIMLOOP:sch 1(A1, A4, A7, A17);
 hence for f being Function of Q,Q st f in Mlt (Nucl Q) holds
ex u, v being Element of Q st
( u in Nucl Q & v in Nucl Q & ( for x being Element of Q holds f . x = u * (x * v) ) ) ; :: thesis: verum