Step |
Hyp |
Ref |
Expression |
1 |
|
srgpcomp.s |
|- S = ( Base ` R ) |
2 |
|
srgpcomp.m |
|- .X. = ( .r ` R ) |
3 |
|
srgpcomp.g |
|- G = ( mulGrp ` R ) |
4 |
|
srgpcomp.e |
|- .^ = ( .g ` G ) |
5 |
|
srgpcomp.r |
|- ( ph -> R e. SRing ) |
6 |
|
srgpcomp.a |
|- ( ph -> A e. S ) |
7 |
|
srgpcomp.b |
|- ( ph -> B e. S ) |
8 |
|
srgpcomp.k |
|- ( ph -> K e. NN0 ) |
9 |
|
srgpcomp.c |
|- ( ph -> ( A .X. B ) = ( B .X. A ) ) |
10 |
|
srgpcompp.n |
|- ( ph -> N e. NN0 ) |
11 |
|
srgpcomppsc.t |
|- .x. = ( .g ` R ) |
12 |
|
srgpcomppsc.c |
|- ( ph -> C e. NN0 ) |
13 |
3
|
srgmgp |
|- ( R e. SRing -> G e. Mnd ) |
14 |
5 13
|
syl |
|- ( ph -> G e. Mnd ) |
15 |
3 1
|
mgpbas |
|- S = ( Base ` G ) |
16 |
15 4
|
mulgnn0cl |
|- ( ( G e. Mnd /\ N e. NN0 /\ A e. S ) -> ( N .^ A ) e. S ) |
17 |
14 10 6 16
|
syl3anc |
|- ( ph -> ( N .^ A ) e. S ) |
18 |
15 4
|
mulgnn0cl |
|- ( ( G e. Mnd /\ K e. NN0 /\ B e. S ) -> ( K .^ B ) e. S ) |
19 |
14 8 7 18
|
syl3anc |
|- ( ph -> ( K .^ B ) e. S ) |
20 |
1 11 2
|
srgmulgass |
|- ( ( R e. SRing /\ ( C e. NN0 /\ ( N .^ A ) e. S /\ ( K .^ B ) e. S ) ) -> ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) = ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) ) |
21 |
20
|
eqcomd |
|- ( ( R e. SRing /\ ( C e. NN0 /\ ( N .^ A ) e. S /\ ( K .^ B ) e. S ) ) -> ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) = ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) ) |
22 |
5 12 17 19 21
|
syl13anc |
|- ( ph -> ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) = ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) ) |
23 |
22
|
oveq1d |
|- ( ph -> ( ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) .X. A ) = ( ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) .X. A ) ) |
24 |
|
srgmnd |
|- ( R e. SRing -> R e. Mnd ) |
25 |
5 24
|
syl |
|- ( ph -> R e. Mnd ) |
26 |
1 11
|
mulgnn0cl |
|- ( ( R e. Mnd /\ C e. NN0 /\ ( N .^ A ) e. S ) -> ( C .x. ( N .^ A ) ) e. S ) |
27 |
25 12 17 26
|
syl3anc |
|- ( ph -> ( C .x. ( N .^ A ) ) e. S ) |
28 |
1 2
|
srgass |
|- ( ( R e. SRing /\ ( ( C .x. ( N .^ A ) ) e. S /\ ( K .^ B ) e. S /\ A e. S ) ) -> ( ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) .X. A ) = ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) ) |
29 |
5 27 19 6 28
|
syl13anc |
|- ( ph -> ( ( ( C .x. ( N .^ A ) ) .X. ( K .^ B ) ) .X. A ) = ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) ) |
30 |
23 29
|
eqtrd |
|- ( ph -> ( ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) .X. A ) = ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) ) |
31 |
1 2
|
srgcl |
|- ( ( R e. SRing /\ ( K .^ B ) e. S /\ A e. S ) -> ( ( K .^ B ) .X. A ) e. S ) |
32 |
5 19 6 31
|
syl3anc |
|- ( ph -> ( ( K .^ B ) .X. A ) e. S ) |
33 |
1 11 2
|
srgmulgass |
|- ( ( R e. SRing /\ ( C e. NN0 /\ ( N .^ A ) e. S /\ ( ( K .^ B ) .X. A ) e. S ) ) -> ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) = ( C .x. ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) ) ) |
34 |
5 12 17 32 33
|
syl13anc |
|- ( ph -> ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) = ( C .x. ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) ) ) |
35 |
1 2
|
srgass |
|- ( ( R e. SRing /\ ( ( N .^ A ) e. S /\ ( K .^ B ) e. S /\ A e. S ) ) -> ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) = ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) ) |
36 |
5 17 19 6 35
|
syl13anc |
|- ( ph -> ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) = ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) ) |
37 |
36
|
eqcomd |
|- ( ph -> ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) = ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) ) |
38 |
37
|
oveq2d |
|- ( ph -> ( C .x. ( ( N .^ A ) .X. ( ( K .^ B ) .X. A ) ) ) = ( C .x. ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) ) ) |
39 |
34 38
|
eqtrd |
|- ( ph -> ( ( C .x. ( N .^ A ) ) .X. ( ( K .^ B ) .X. A ) ) = ( C .x. ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) ) ) |
40 |
1 2 3 4 5 6 7 8 9 10
|
srgpcompp |
|- ( ph -> ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) = ( ( ( N + 1 ) .^ A ) .X. ( K .^ B ) ) ) |
41 |
40
|
oveq2d |
|- ( ph -> ( C .x. ( ( ( N .^ A ) .X. ( K .^ B ) ) .X. A ) ) = ( C .x. ( ( ( N + 1 ) .^ A ) .X. ( K .^ B ) ) ) ) |
42 |
30 39 41
|
3eqtrd |
|- ( ph -> ( ( C .x. ( ( N .^ A ) .X. ( K .^ B ) ) ) .X. A ) = ( C .x. ( ( ( N + 1 ) .^ A ) .X. ( K .^ B ) ) ) ) |