let n be Element of NAT ; for A, B being Ring
for z being Element of A st A is Subring of B holds
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
let A, B be Ring; for z being Element of A st A is Subring of B holds
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
let z be Element of A; ( A is Subring of B implies (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B) )
assume A0:
A is Subring of B
; (power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
then
z is Element of B
by Lm6;
then A2:
In (z,B) = z
by SUBSET_1:def 8;
A3:
1_ A = 1_ B
by A0, C0SP1:def 3;
reconsider x = z as Element of B by A0, Lm6;
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
proof
defpred S1[
Nat]
means (power B) . (
(In (z,B)),$1)
= In (
((power A) . (z,$1)),
B);
A5:
S1[
0 ]
A7:
for
m being
Nat st
S1[
m] holds
S1[
m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A9:
S1[
m]
;
S1[m + 1]
A10:
(power A) . (
z,
m) is
Element of
B
by A0, Lm6;
A11:
In (
((power A) . (z,m)),
B)
= (power A) . (
z,
m)
by A10, SUBSET_1:def 8;
A12:
(power A) . (
z,
(m + 1)) is
Element of
B
by A0, Lm6;
(power B) . (
(In (z,B)),
(m + 1)) =
((power B) . ((In (z,B)),m)) * (In (z,B))
by GROUP_1:def 7
.=
((power A) . (z,m)) * z
by A0, A11, A2, Th9, A9
.=
(power A) . (
z,
(m + 1))
by GROUP_1:def 7
.=
In (
((power A) . (z,(m + 1))),
B)
by A12, SUBSET_1:def 8
;
hence
S1[
m + 1]
;
verum
end;
for
m being
Nat holds
S1[
m]
from NAT_1:sch 2(A5, A7);
hence
(power B) . (
(In (z,B)),
n)
= In (
((power A) . (z,n)),
B)
;
verum
end;
hence
(power B) . ((In (z,B)),n) = In (((power A) . (z,n)),B)
; verum