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 )