let Q be multLoop; :: thesis: for N being SubLoop of Q
for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds
for x being Element of Q holds
( x in @ ([#] N) iff f . x in @ ([#] N) )
let N be SubLoop of Q; :: thesis: for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds
for x being Element of Q holds
( x in @ ([#] N) iff f . x in @ ([#] N) )
reconsider H = @ ([#] N) as Subset of Q ;
defpred S3[ Function of Q,Q] means for x being Element of Q holds
( x in H iff $1 . x in H );
A1: for u being Element of Q st u in H 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 H 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 H ; :: 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]
S3[f]
proof
let x be Element of Q; :: thesis: ( x in H iff f . x in H )
thus ( x in H implies f . x in H ) :: thesis: ( f . x in H implies x in H )
proof
assume x in H ; :: thesis: f . x in H
then x * u in the carrier of N by Th37, A2;
hence f . x in H by A3; :: thesis: verum
end;
assume f . x in H ; :: thesis: x in H
then reconsider xu1 = x * u as Element of N by A3;
reconsider u1 = u as Element of N by A2;
the carrier of N c= the carrier of Q by Def30;
then reconsider xu1u1 = xu1 / u1 as Element of Q ;
A4: x * u = (xu1 / u1) * u1
.= xu1u1 * u by Th36 ;
x = (xu1u1 * u) / u by A4
.= xu1 / u1 ;
hence x in H ; :: thesis: verum
end;
hence S3[f] ; :: thesis: verum
end;
A5: for u being Element of Q st u in H 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 H implies for f being Function of Q,Q st ( for x being Element of Q holds f . x = u * x ) holds
S3[f] )
assume A6: u in H ; :: 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 A7: for x being Element of Q holds f . x = u * x ; :: thesis: S3[f]
S3[f]
proof
let x be Element of Q; :: thesis: ( x in H iff f . x in H )
thus ( x in H implies f . x in H ) :: thesis: ( f . x in H implies x in H )
proof
assume x in H ; :: thesis: f . x in H
then u * x in the carrier of N by Th37, A6;
hence f . x in H by A7; :: thesis: verum
end;
assume f . x in H ; :: thesis: x in H
then reconsider ux1 = u * x, u1 = u as Element of N by A7, A6;
the carrier of N c= the carrier of Q by Def30;
then reconsider u1ux1 = u1 \ ux1 as Element of Q ;
u * x = u1 * (u1 \ ux1)
.= u * u1ux1 by Th36 ;
then x = u \ (u * u1ux1)
.= u1 \ ux1 ;
hence x in H ; :: thesis: verum
end;
hence S3[f] ; :: thesis: verum
end;
A8: for g, h being Permutation of Q st S3[g] & S3[h] holds
S3[g * h]
proof
let g, h be Permutation of Q; :: thesis: ( S3[g] & S3[h] implies S3[g * h] )
assume A9: ( S3[g] & S3[h] ) ; :: thesis: S3[g * h]
let x be Element of Q; :: thesis: ( x in H iff (g * h) . x in H )
( x in H iff h . x in H ) by A9;
then ( x in H iff g . (h . x) in H ) by A9;
hence ( x in H iff (g * h) . x in H ) by FUNCT_2:15; :: thesis: verum
end;
A10: 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 A11: S3[g] ; :: thesis: S3[g " ]
let x be Element of Q; :: thesis: ( x in H iff (g ") . x in H )
x = (id the carrier of Q) . x
.= (g * (g ")) . x by FUNCT_2:61
.= g . ((g ") . x) by FUNCT_2:15 ;
hence ( x in H iff (g ") . x in H ) by A11; :: thesis: verum
end;
for f being Function of Q,Q st f in Mlt H holds
S3[f] from AIMLOOP:sch 1(A1, A5, A8, A10);
 hence for f being Function of Q,Q st f in Mlt (@ ([#] N)) holds
for x being Element of Q holds
( x in @ ([#] N) iff f . x in @ ([#] N) ) ; :: thesis: verum