srgbinomlem1

	Ref	Expression
Hypotheses	srgbinom.s	$⊢ S = {Base}_{R}$
	srgbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
	srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
	srgbinom.g	$⊢ G = {mulGrp}_{R}$
	srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
	srgbinomlem.r	$⊢ φ \to R \in SRing$
	srgbinomlem.a	$⊢ φ \to A \in S$
	srgbinomlem.b	$⊢ φ \to B \in S$
	srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
	srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
Assertion	srgbinomlem1	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to (D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B) \in S$

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	$⊢ S = {Base}_{R}$
2		srgbinom.m	$⊢ \underset{˙}{\times} = \cdot_{R}$
3		srgbinom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		srgbinom.a	$⊢ \underset{˙}{+} = +_{R}$
5		srgbinom.g	$⊢ G = {mulGrp}_{R}$
6		srgbinom.e	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		srgbinomlem.r	$⊢ φ \to R \in SRing$
8		srgbinomlem.a	$⊢ φ \to A \in S$
9		srgbinomlem.b	$⊢ φ \to B \in S$
10		srgbinomlem.c	$⊢ φ \to A \underset{˙}{\times} B = B \underset{˙}{\times} A$
11		srgbinomlem.n	$⊢ φ \to N \in ℕ_{0}$
12	7	adantr	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to R \in SRing$
13	5 1	mgpbas	$⊢ S = {Base}_{G}$
14	5	srgmgp	$⊢ R \in SRing \to G \in Mnd$
15	7 14	syl	$⊢ φ \to G \in Mnd$
16	15	adantr	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to G \in Mnd$
17		simprl	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to D \in ℕ_{0}$
18	8	adantr	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to A \in S$
19	13 6 16 17 18	mulgnn0cld	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to D \underset{˙}{\times} A \in S$
20		simprr	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to E \in ℕ_{0}$
21	9	adantr	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to B \in S$
22	13 6 16 20 21	mulgnn0cld	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to E \underset{˙}{\times} B \in S$
23	1 2	srgcl	$⊢ (R \in SRing \land D \underset{˙}{\times} A \in S \land E \underset{˙}{\times} B \in S) \to (D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B) \in S$
24	12 19 22 23	syl3anc	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to (D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B) \in S$

Metamath Proof Explorer

Theorem srgbinomlem1

Proof