Theorem srgbinomlem1

Description: Lemma 1 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	srgbinomlem1	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ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	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝑅 ∈ SRing )
13	5 1	mgpbas	⊢ 𝑆 = ( Base ‘ 𝐺 )
14	5	srgmgp	⊢ ( 𝑅 ∈ SRing → 𝐺 ∈ Mnd )
15	7 14	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐺 ∈ Mnd )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐷 ∈ ℕ0 )
18	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐴 ∈ 𝑆 )
19	13 6 16 17 18	mulgnn0cld	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( 𝐷 ↑ 𝐴 ) ∈ 𝑆 )
20		simprr	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐸 ∈ ℕ0 )
21	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → 𝐵 ∈ 𝑆 )
22	13 6 16 20 21	mulgnn0cld	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( 𝐸 ↑ 𝐵 ) ∈ 𝑆 )
23	1 2	srgcl	⊢ ( ( 𝑅 ∈ SRing ∧ ( 𝐷 ↑ 𝐴 ) ∈ 𝑆 ∧ ( 𝐸 ↑ 𝐵 ) ∈ 𝑆 ) → ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 )
24	12 19 22 23	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 )