let n be Nat; for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS holds
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
let RAS be non empty MidSp-like ReperAlgebraStr over n + 2; for W being ATLAS of RAS holds
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
let W be ATLAS of RAS; ( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
A1:
( ( for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) ) implies RAS is being_invariance )
proof
assume A2:
for
a,
b being
Point of
RAS for
x being
Tuple of
(n + 1),
W holds
Phi (
a,
x)
= Phi (
b,
x)
;
RAS is being_invariance
let a be
Point of
RAS;
MIDSP_3:def 3 for b being Point of RAS
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p))let b be
Point of
RAS;
for p, q being Tuple of (n + 1),RAS st ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) holds
a @ (*' (b,q)) = b @ (*' (a,p))let p,
q be
Tuple of
(n + 1),
RAS;
( ( for m being Nat of n holds a @ (q . m) = b @ (p . m) ) implies a @ (*' (b,q)) = b @ (*' (a,p)) )
A3:
W . (
a,
(*' (a,((a,(W . (a,p))) . W)))) =
Phi (
a,
(W . (a,p)))
.=
Phi (
b,
(W . (a,p)))
by A2
.=
W . (
b,
(*' (b,((b,(W . (a,p))) . W))))
;
assume A4:
for
m being
Nat of
n holds
a @ (q . m) = b @ (p . m)
;
a @ (*' (b,q)) = b @ (*' (a,p))
A5:
now for m being Nat of n holds (W . (a,p)) . m = (W . (b,q)) . mend;
W . (
a,
(*' (a,p))) =
W . (
a,
(*' (a,((a,(W . (a,p))) . W))))
by Th15
.=
W . (
b,
(*' (b,((b,(W . (b,q))) . W))))
by A5, A3, Th14
.=
W . (
b,
(*' (b,q)))
by Th15
;
hence
a @ (*' (b,q)) = b @ (*' (a,p))
by MIDSP_2:33;
verum
end;
now ( RAS is being_invariance implies for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )assume A7:
RAS is
being_invariance
;
for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)let a,
b be
Point of
RAS;
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x)let x be
Tuple of
(n + 1),
W;
Phi (a,x) = Phi (b,x)set p = (
a,
x)
. W;
set q = (
b,
x)
. W;
A8:
W . (
a,
((a,x) . W)) =
x
by Th15
.=
W . (
b,
((b,x) . W))
by Th15
;
now for m being Nat of n holds a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)let m be
Nat of
n;
a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)W . (
a,
(((a,x) . W) . m)) =
(W . (a,((a,x) . W))) . m
by Def9
.=
W . (
b,
(((b,x) . W) . m))
by A8, Def9
;
hence
a @ (((b,x) . W) . m) = b @ (((a,x) . W) . m)
by MIDSP_2:33;
verum end; then
a @ (*' (b,((b,x) . W))) = b @ (*' (a,((a,x) . W)))
by A7;
hence
Phi (
a,
x)
= Phi (
b,
x)
by MIDSP_2:33;
verum end;
hence
( RAS is being_invariance iff for a, b being Point of RAS
for x being Tuple of (n + 1),W holds Phi (a,x) = Phi (b,x) )
by A1; verum