srgbinomlem2

	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	srgbinomlem2	$⊢ (φ \land (C \in ℕ_{0} \land D \in ℕ_{0} \land E \in ℕ_{0})) \to C \underset{˙}{\cdot} ((D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B)) \in S$

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		srgmnd	$⊢ R \in SRing \to R \in Mnd$
13	7 12	syl	$⊢ φ \to R \in Mnd$
14	13	adantr	$⊢ (φ \land (C \in ℕ_{0} \land D \in ℕ_{0} \land E \in ℕ_{0})) \to R \in Mnd$
15		simpr1	$⊢ (φ \land (C \in ℕ_{0} \land D \in ℕ_{0} \land E \in ℕ_{0})) \to C \in ℕ_{0}$
16	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem1	$⊢ (φ \land (D \in ℕ_{0} \land E \in ℕ_{0})) \to (D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B) \in S$
17	16	3adantr1	$⊢ (φ \land (C \in ℕ_{0} \land D \in ℕ_{0} \land E \in ℕ_{0})) \to (D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B) \in S$
18	1 3 14 15 17	mulgnn0cld	$⊢ (φ \land (C \in ℕ_{0} \land D \in ℕ_{0} \land E \in ℕ_{0})) \to C \underset{˙}{\cdot} ((D \underset{˙}{\times} A) \underset{˙}{\times} (E \underset{˙}{\times} B)) \in S$

Metamath Proof Explorer