Theorem srgbinomlem1

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

	Ref	Expression
Hypotheses	srgbinom.s	$$⊢S={\mathrm{Base}}_R$$
	srgbinom.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
	srgbinom.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	srgbinom.a	$$⊢\underset{\dot{}}{+}={+}_R$$
	srgbinom.g	$$⊢G={\mathrm{mulGrp}}_R$$
	srgbinom.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
	srgbinomlem.r	$$⊢\phi \to R\in \mathrm{SRing}$$
	srgbinomlem.a	$$⊢\phi \to A\in S$$
	srgbinomlem.b	$$⊢\phi \to B\in S$$
	srgbinomlem.c	$$⊢\phi \to A\underset{\dot{}}{\times }B=B\underset{\dot{}}{\times }A$$
	srgbinomlem.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	srgbinomlem1	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to \left(D\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(E\underset{\dot{}}{\times }B\right)\in S$$

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	$$⊢S={\mathrm{Base}}_R$$
2		srgbinom.m	$$⊢\underset{\dot{}}{\times }={\cdot }_R$$
3		srgbinom.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		srgbinom.a	$$⊢\underset{\dot{}}{+}={+}_R$$
5		srgbinom.g	$$⊢G={\mathrm{mulGrp}}_R$$
6		srgbinom.e	$$⊢\underset{\dot{}}{\times }={\cdot }_G$$
7		srgbinomlem.r	$$⊢\phi \to R\in \mathrm{SRing}$$
8		srgbinomlem.a	$$⊢\phi \to A\in S$$
9		srgbinomlem.b	$$⊢\phi \to B\in S$$
10		srgbinomlem.c	$$⊢\phi \to A\underset{\dot{}}{\times }B=B\underset{\dot{}}{\times }A$$
11		srgbinomlem.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12	7	adantr	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to R\in \mathrm{SRing}$$
13	5	srgmgp	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$
14	7 13	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
15	14	adantr	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to G\in \mathrm{Mnd}$$
16		simprl	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to D\in {\mathbb{N}}_0$$
17	8	adantr	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to A\in S$$
18	5 1	mgpbas	$$⊢S={\mathrm{Base}}_G$$
19	18 6	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge D\in {\mathbb{N}}_0\wedge A\in S\right)\to D\underset{\dot{}}{\times }A\in S$$
20	15 16 17 19	syl3anc	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to D\underset{\dot{}}{\times }A\in S$$
21		simprr	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to E\in {\mathbb{N}}_0$$
22	9	adantr	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to B\in S$$
23	18 6	mulgnn0cl	$$⊢\left(G\in \mathrm{Mnd}\wedge E\in {\mathbb{N}}_0\wedge B\in S\right)\to E\underset{\dot{}}{\times }B\in S$$
24	15 21 22 23	syl3anc	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to E\underset{\dot{}}{\times }B\in S$$
25	1 2	srgcl	$$⊢\left(R\in \mathrm{SRing}\wedge D\underset{\dot{}}{\times }A\in S\wedge E\underset{\dot{}}{\times }B\in S\right)\to \left(D\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(E\underset{\dot{}}{\times }B\right)\in S$$
26	12 20 24 25	syl3anc	$$⊢\left(\phi \wedge \left(D\in {\mathbb{N}}_0\wedge E\in {\mathbb{N}}_0\right)\right)\to \left(D\underset{\dot{}}{\times }A\right)\underset{\dot{}}{\times }\left(E\underset{\dot{}}{\times }B\right)\in S$$