| 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 |
|
srgmnd |
|- ( R e. SRing -> R e. Mnd ) |
| 13 |
7 12
|
syl |
|- ( ph -> R e. Mnd ) |
| 14 |
13
|
adantr |
|- ( ( ph /\ ( C e. NN0 /\ D e. NN0 /\ E e. NN0 ) ) -> R e. Mnd ) |
| 15 |
|
simpr1 |
|- ( ( ph /\ ( C e. NN0 /\ D e. NN0 /\ E e. NN0 ) ) -> C e. NN0 ) |
| 16 |
1 2 3 4 5 6 7 8 9 10 11
|
srgbinomlem1 |
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S ) |
| 17 |
16
|
3adantr1 |
|- ( ( ph /\ ( C e. NN0 /\ D e. NN0 /\ E e. NN0 ) ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S ) |
| 18 |
1 3 14 15 17
|
mulgnn0cld |
|- ( ( ph /\ ( C e. NN0 /\ D e. NN0 /\ E e. NN0 ) ) -> ( C .x. ( ( D .^ A ) .X. ( E .^ B ) ) ) e. S ) |