Metamath Proof Explorer


Theorem srgbinomlem1

Description: Lemma 1 for srgbinomlem . (Contributed by AV, 23-Aug-2019)

Ref Expression
Hypotheses srgbinom.s
|- S = ( Base ` R )
srgbinom.m
|- .X. = ( .r ` R )
srgbinom.t
|- .x. = ( .g ` R )
srgbinom.a
|- .+ = ( +g ` R )
srgbinom.g
|- G = ( mulGrp ` R )
srgbinom.e
|- .^ = ( .g ` G )
srgbinomlem.r
|- ( ph -> R e. SRing )
srgbinomlem.a
|- ( ph -> A e. S )
srgbinomlem.b
|- ( ph -> B e. S )
srgbinomlem.c
|- ( ph -> ( A .X. B ) = ( B .X. A ) )
srgbinomlem.n
|- ( ph -> N e. NN0 )
Assertion srgbinomlem1
|- ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S )

Proof

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 1 mgpbas
 |-  S = ( Base ` G )
14 5 srgmgp
 |-  ( R e. SRing -> G e. Mnd )
15 7 14 syl
 |-  ( ph -> G e. Mnd )
16 15 adantr
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> G e. Mnd )
17 simprl
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> D e. NN0 )
18 8 adantr
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> A e. S )
19 13 6 16 17 18 mulgnn0cld
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( D .^ A ) e. S )
20 simprr
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> E e. NN0 )
21 9 adantr
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> B e. S )
22 13 6 16 20 21 mulgnn0cld
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( E .^ B ) e. S )
23 1 2 srgcl
 |-  ( ( R e. SRing /\ ( D .^ A ) e. S /\ ( E .^ B ) e. S ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S )
24 12 19 22 23 syl3anc
 |-  ( ( ph /\ ( D e. NN0 /\ E e. NN0 ) ) -> ( ( D .^ A ) .X. ( E .^ B ) ) e. S )