This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) → ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ∈ 𝑆 )