Theorem srgbinomlem2

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

	Ref	Expression
Hypotheses	srgbinom.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
	srgbinom.m	⊢ × = ( .r ‘ 𝑅 )
	srgbinom.t	⊢ · = ( .g ‘ 𝑅 )
	srgbinom.a	⊢ + = ( +g ‘ 𝑅 )
	srgbinom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
	srgbinom.e	⊢ ↑ = ( .g ‘ 𝐺 )
	srgbinomlem.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
	srgbinomlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	srgbinomlem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	srgbinomlem.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
	srgbinomlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	srgbinomlem2	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( 𝐶 · ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		srgbinom.s	⊢ 𝑆 = ( Base ‘ 𝑅 )
2		srgbinom.m	⊢ × = ( .r ‘ 𝑅 )
3		srgbinom.t	⊢ · = ( .g ‘ 𝑅 )
4		srgbinom.a	⊢ + = ( +g ‘ 𝑅 )
5		srgbinom.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
6		srgbinom.e	⊢ ↑ = ( .g ‘ 𝐺 )
7		srgbinomlem.r	⊢ ( 𝜑 → 𝑅 ∈ SRing )
8		srgbinomlem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
9		srgbinomlem.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
10		srgbinomlem.c	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 ) )
11		srgbinomlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12		srgmnd	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ Mnd )
13	7 12	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
14	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝑅 ∈ Mnd )
15		simpr1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐶 ∈ ℕ0 )
16	1 2 3 4 5 6 7 8 9 10 11	srgbinomlem1	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 )
17	16	3adantr1	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 )
18	1 3	mulgnn0cl	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝐶 ∈ ℕ0 ∧ ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 ) → ( 𝐶 · ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ) ∈ 𝑆 )
19	14 15 17 18	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( 𝐶 · ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ) ∈ 𝑆 )