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