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

Metamath Proof Explorer

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 14 15 17 mulgnn0cld ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ) ) → ( 𝐶 · ( ( 𝐷 ↑ 𝐴 ) × ( 𝐸 ↑ 𝐵 ) ) ) ∈ 𝑆 )