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