Metamath Proof Explorer


Theorem srgbinomlem

Description: Lemma for srgbinom . Inductive step, analogous to binomlem . (Contributed by AV, 24-Aug-2019)

Ref Expression
Hypotheses srgbinom.s S = Base R
srgbinom.m × ˙ = R
srgbinom.t · ˙ = R
srgbinom.a + ˙ = + R
srgbinom.g G = mulGrp R
srgbinom.e × ˙ = G
srgbinomlem.r φ R SRing
srgbinomlem.a φ A S
srgbinomlem.b φ B S
srgbinomlem.c φ A × ˙ B = B × ˙ A
srgbinomlem.n φ N 0
srgbinomlem.i ψ N × ˙ A + ˙ B = R k = 0 N ( N k) · ˙ N k × ˙ A × ˙ k × ˙ B
Assertion srgbinomlem φ ψ N + 1 × ˙ A + ˙ B = R k = 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B

Proof

Step Hyp Ref Expression
1 srgbinom.s S = Base R
2 srgbinom.m × ˙ = R
3 srgbinom.t · ˙ = R
4 srgbinom.a + ˙ = + R
5 srgbinom.g G = mulGrp R
6 srgbinom.e × ˙ = G
7 srgbinomlem.r φ R SRing
8 srgbinomlem.a φ A S
9 srgbinomlem.b φ B S
10 srgbinomlem.c φ A × ˙ B = B × ˙ A
11 srgbinomlem.n φ N 0
12 srgbinomlem.i ψ N × ˙ A + ˙ B = R k = 0 N ( N k) · ˙ N k × ˙ A × ˙ k × ˙ B
13 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem3 φ ψ N × ˙ A + ˙ B × ˙ A = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
14 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem4 φ ψ N × ˙ A + ˙ B × ˙ B = R k = 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
15 13 14 oveq12d φ ψ N × ˙ A + ˙ B × ˙ A + ˙ N × ˙ A + ˙ B × ˙ B = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ R k = 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
16 5 srgmgp R SRing G Mnd
17 7 16 syl φ G Mnd
18 srgmnd R SRing R Mnd
19 7 18 syl φ R Mnd
20 1 4 mndcl R Mnd A S B S A + ˙ B S
21 19 8 9 20 syl3anc φ A + ˙ B S
22 17 11 21 3jca φ G Mnd N 0 A + ˙ B S
23 22 adantr φ ψ G Mnd N 0 A + ˙ B S
24 5 1 mgpbas S = Base G
25 5 2 mgpplusg × ˙ = + G
26 24 6 25 mulgnn0p1 G Mnd N 0 A + ˙ B S N + 1 × ˙ A + ˙ B = N × ˙ A + ˙ B × ˙ A + ˙ B
27 23 26 syl φ ψ N + 1 × ˙ A + ˙ B = N × ˙ A + ˙ B × ˙ A + ˙ B
28 24 6 17 11 21 mulgnn0cld φ N × ˙ A + ˙ B S
29 28 8 9 3jca φ N × ˙ A + ˙ B S A S B S
30 7 29 jca φ R SRing N × ˙ A + ˙ B S A S B S
31 30 adantr φ ψ R SRing N × ˙ A + ˙ B S A S B S
32 1 4 2 srgdi R SRing N × ˙ A + ˙ B S A S B S N × ˙ A + ˙ B × ˙ A + ˙ B = N × ˙ A + ˙ B × ˙ A + ˙ N × ˙ A + ˙ B × ˙ B
33 31 32 syl φ ψ N × ˙ A + ˙ B × ˙ A + ˙ B = N × ˙ A + ˙ B × ˙ A + ˙ N × ˙ A + ˙ B × ˙ B
34 27 33 eqtrd φ ψ N + 1 × ˙ A + ˙ B = N × ˙ A + ˙ B × ˙ A + ˙ N × ˙ A + ˙ B × ˙ B
35 elfzelz k 0 N + 1 k
36 bcpasc N 0 k ( N k) + ( N k 1 ) = ( N + 1 k)
37 11 35 36 syl2an φ k 0 N + 1 ( N k) + ( N k 1 ) = ( N + 1 k)
38 37 oveq1d φ k 0 N + 1 ( N k) + ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
39 19 adantr φ k 0 N + 1 R Mnd
40 bccl N 0 k ( N k) 0
41 11 35 40 syl2an φ k 0 N + 1 ( N k) 0
42 35 adantl φ k 0 N + 1 k
43 peano2zm k k 1
44 42 43 syl φ k 0 N + 1 k 1
45 bccl N 0 k 1 ( N k 1 ) 0
46 11 44 45 syl2an2r φ k 0 N + 1 ( N k 1 ) 0
47 7 adantr φ k 0 N + 1 R SRing
48 17 adantr φ k 0 N + 1 G Mnd
49 fznn0sub k 0 N + 1 N + 1 - k 0
50 49 adantl φ k 0 N + 1 N + 1 - k 0
51 8 adantr φ k 0 N + 1 A S
52 24 6 48 50 51 mulgnn0cld φ k 0 N + 1 N + 1 - k × ˙ A S
53 elfznn0 k 0 N + 1 k 0
54 53 adantl φ k 0 N + 1 k 0
55 9 adantr φ k 0 N + 1 B S
56 24 6 48 54 55 mulgnn0cld φ k 0 N + 1 k × ˙ B S
57 1 2 srgcl R SRing N + 1 - k × ˙ A S k × ˙ B S N + 1 - k × ˙ A × ˙ k × ˙ B S
58 47 52 56 57 syl3anc φ k 0 N + 1 N + 1 - k × ˙ A × ˙ k × ˙ B S
59 1 3 4 mulgnn0dir R Mnd ( N k) 0 ( N k 1 ) 0 N + 1 - k × ˙ A × ˙ k × ˙ B S ( N k) + ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
60 39 41 46 58 59 syl13anc φ k 0 N + 1 ( N k) + ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
61 38 60 eqtr3d φ k 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
62 61 mpteq2dva φ k 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = k 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
63 62 oveq2d φ R k = 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
64 srgcmn R SRing R CMnd
65 7 64 syl φ R CMnd
66 fzfid φ 0 N + 1 Fin
67 1 3 39 41 58 mulgnn0cld φ k 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B S
68 35 43 syl k 0 N + 1 k 1
69 11 68 45 syl2an φ k 0 N + 1 ( N k 1 ) 0
70 1 3 39 69 58 mulgnn0cld φ k 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B S
71 eqid k 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = k 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
72 eqid k 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = k 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
73 1 4 65 66 67 70 71 72 gsummptfidmadd φ R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ R k = 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
74 63 73 eqtrd φ R k = 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ R k = 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
75 74 adantr φ ψ R k = 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B = R k = 0 N + 1 ( N k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B + ˙ R k = 0 N + 1 ( N k 1 ) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B
76 15 34 75 3eqtr4d φ ψ N + 1 × ˙ A + ˙ B = R k = 0 N + 1 ( N + 1 k) · ˙ N + 1 - k × ˙ A × ˙ k × ˙ B