| Step |
Hyp |
Ref |
Expression |
| 1 |
|
srgbinom.s |
|- S = ( Base ` R ) |
| 2 |
|
srgbinom.m |
|- .X. = ( .r ` R ) |
| 3 |
|
srgbinom.t |
|- .x. = ( .g ` R ) |
| 4 |
|
srgbinom.a |
|- .+ = ( +g ` R ) |
| 5 |
|
srgbinom.g |
|- G = ( mulGrp ` R ) |
| 6 |
|
srgbinom.e |
|- .^ = ( .g ` G ) |
| 7 |
|
srgbinomlem.r |
|- ( ph -> R e. SRing ) |
| 8 |
|
srgbinomlem.a |
|- ( ph -> A e. S ) |
| 9 |
|
srgbinomlem.b |
|- ( ph -> B e. S ) |
| 10 |
|
srgbinomlem.c |
|- ( ph -> ( A .X. B ) = ( B .X. A ) ) |
| 11 |
|
srgbinomlem.n |
|- ( ph -> N e. NN0 ) |
| 12 |
7
|
adantr |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> R e. SRing ) |
| 13 |
5
|
srgmgp |
|- ( R e. SRing -> G e. Mnd ) |
| 14 |
7 13
|
syl |
|- ( ph -> G e. Mnd ) |
| 15 |
14
|
adantr |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> G e. Mnd ) |
| 16 |
|
simprl |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> D e. NN0 ) |
| 17 |
8
|
adantr |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> A e. S ) |
| 18 |
5 1
|
mgpbas |
|- S = ( Base ` G ) |
| 19 |
18 6
|
mulgnn0cl |
|- ( ( G e. Mnd /\ D e. NN0 /\ A e. S ) -> ( D .^ A ) e. S ) |
| 20 |
15 16 17 19
|
syl3anc |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( D .^ A ) e. S ) |
| 21 |
|
simprr |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> E e. NN0 ) |
| 22 |
9
|
adantr |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> B e. S ) |
| 23 |
18 6
|
mulgnn0cl |
|- ( ( G e. Mnd /\ E e. NN0 /\ B e. S ) -> ( E .^ B ) e. S ) |
| 24 |
15 21 22 23
|
syl3anc |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( E .^ B ) e. S ) |
| 25 |
1 2
|
srgcl |
|- ( ( R e. SRing /\ ( D .^ A ) e. S /\ ( E .^ B ) e. S ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S ) |
| 26 |
12 20 24 25
|
syl3anc |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S ) |