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 โŠข ๐‘† = ( 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 )
srgbinomlem.i โŠข ( ๐œ“ โ†’ ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ๐‘ ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ๐‘ โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )
Assertion srgbinomlem ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ + 1 ) โ†‘ ( ๐ด + ๐ต ) ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )

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 srgbinomlem.i โŠข ( ๐œ“ โ†’ ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ๐‘ ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ๐‘ โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem3 โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ด ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )
14 1 2 3 4 5 6 7 8 9 10 11 12 srgbinomlem4 โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ต ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )
15 13 14 oveq12d โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ด ) + ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ต ) ) = ( ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) + ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) )
16 5 srgmgp โŠข ( ๐‘… โˆˆ SRing โ†’ ๐บ โˆˆ Mnd )
17 7 16 syl โŠข ( ๐œ‘ โ†’ ๐บ โˆˆ Mnd )
18 srgmnd โŠข ( ๐‘… โˆˆ SRing โ†’ ๐‘… โˆˆ Mnd )
19 7 18 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Mnd )
20 1 4 mndcl โŠข ( ( ๐‘… โˆˆ Mnd โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† ) โ†’ ( ๐ด + ๐ต ) โˆˆ ๐‘† )
21 19 8 9 20 syl3anc โŠข ( ๐œ‘ โ†’ ( ๐ด + ๐ต ) โˆˆ ๐‘† )
22 17 11 21 3jca โŠข ( ๐œ‘ โ†’ ( ๐บ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ( ๐ด + ๐ต ) โˆˆ ๐‘† ) )
23 22 adantr โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ๐บ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ( ๐ด + ๐ต ) โˆˆ ๐‘† ) )
24 5 1 mgpbas โŠข ๐‘† = ( Base โ€˜ ๐บ )
25 5 2 mgpplusg โŠข ร— = ( +g โ€˜ ๐บ )
26 24 6 25 mulgnn0p1 โŠข ( ( ๐บ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ( ๐ด + ๐ต ) โˆˆ ๐‘† ) โ†’ ( ( ๐‘ + 1 ) โ†‘ ( ๐ด + ๐ต ) ) = ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ( ๐ด + ๐ต ) ) )
27 23 26 syl โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ + 1 ) โ†‘ ( ๐ด + ๐ต ) ) = ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ( ๐ด + ๐ต ) ) )
28 24 6 17 11 21 mulgnn0cld โŠข ( ๐œ‘ โ†’ ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) โˆˆ ๐‘† )
29 28 8 9 3jca โŠข ( ๐œ‘ โ†’ ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) โˆˆ ๐‘† โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† ) )
30 7 29 jca โŠข ( ๐œ‘ โ†’ ( ๐‘… โˆˆ SRing โˆง ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) โˆˆ ๐‘† โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† ) ) )
31 30 adantr โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ๐‘… โˆˆ SRing โˆง ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) โˆˆ ๐‘† โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† ) ) )
32 1 4 2 srgdi โŠข ( ( ๐‘… โˆˆ SRing โˆง ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) โˆˆ ๐‘† โˆง ๐ด โˆˆ ๐‘† โˆง ๐ต โˆˆ ๐‘† ) ) โ†’ ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ( ๐ด + ๐ต ) ) = ( ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ด ) + ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ต ) ) )
33 31 32 syl โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ( ๐ด + ๐ต ) ) = ( ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ด ) + ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ต ) ) )
34 27 33 eqtrd โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ + 1 ) โ†‘ ( ๐ด + ๐ต ) ) = ( ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ด ) + ( ( ๐‘ โ†‘ ( ๐ด + ๐ต ) ) ร— ๐ต ) ) )
35 elfzelz โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†’ ๐‘˜ โˆˆ โ„ค )
36 bcpasc โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( ( ๐‘ C ๐‘˜ ) + ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ) = ( ( ๐‘ + 1 ) C ๐‘˜ ) )
37 11 35 36 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ๐‘ C ๐‘˜ ) + ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ) = ( ( ๐‘ + 1 ) C ๐‘˜ ) )
38 37 oveq1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ( ๐‘ C ๐‘˜ ) + ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) = ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) )
39 19 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐‘… โˆˆ Mnd )
40 bccl โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( ๐‘ C ๐‘˜ ) โˆˆ โ„•0 )
41 11 35 40 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ๐‘ C ๐‘˜ ) โˆˆ โ„•0 )
42 35 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐‘˜ โˆˆ โ„ค )
43 peano2zm โŠข ( ๐‘˜ โˆˆ โ„ค โ†’ ( ๐‘˜ โˆ’ 1 ) โˆˆ โ„ค )
44 42 43 syl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ๐‘˜ โˆ’ 1 ) โˆˆ โ„ค )
45 bccl โŠข ( ( ๐‘ โˆˆ โ„•0 โˆง ( ๐‘˜ โˆ’ 1 ) โˆˆ โ„ค ) โ†’ ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) โˆˆ โ„•0 )
46 11 44 45 syl2an2r โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) โˆˆ โ„•0 )
47 7 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐‘… โˆˆ SRing )
48 17 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐บ โˆˆ Mnd )
49 fznn0sub โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†’ ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โˆˆ โ„•0 )
50 49 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โˆˆ โ„•0 )
51 8 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐ด โˆˆ ๐‘† )
52 24 6 48 50 51 mulgnn0cld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) โˆˆ ๐‘† )
53 elfznn0 โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
54 53 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
55 9 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ๐ต โˆˆ ๐‘† )
56 24 6 48 54 55 mulgnn0cld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ๐‘˜ โ†‘ ๐ต ) โˆˆ ๐‘† )
57 1 2 srgcl โŠข ( ( ๐‘… โˆˆ SRing โˆง ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) โˆˆ ๐‘† โˆง ( ๐‘˜ โ†‘ ๐ต ) โˆˆ ๐‘† ) โ†’ ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) โˆˆ ๐‘† )
58 47 52 56 57 syl3anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) โˆˆ ๐‘† )
59 1 3 4 mulgnn0dir โŠข ( ( ๐‘… โˆˆ Mnd โˆง ( ( ๐‘ C ๐‘˜ ) โˆˆ โ„•0 โˆง ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) โˆˆ โ„•0 โˆง ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) โˆˆ ๐‘† ) ) โ†’ ( ( ( ๐‘ C ๐‘˜ ) + ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) = ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) )
60 39 41 46 58 59 syl13anc โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ( ๐‘ C ๐‘˜ ) + ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) = ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) )
61 38 60 eqtr3d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) = ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) )
62 61 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) = ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )
63 62 oveq2d โŠข ( ๐œ‘ โ†’ ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) )
64 srgcmn โŠข ( ๐‘… โˆˆ SRing โ†’ ๐‘… โˆˆ CMnd )
65 7 64 syl โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ CMnd )
66 fzfid โŠข ( ๐œ‘ โ†’ ( 0 ... ( ๐‘ + 1 ) ) โˆˆ Fin )
67 1 3 39 41 58 mulgnn0cld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) โˆˆ ๐‘† )
68 35 43 syl โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†’ ( ๐‘˜ โˆ’ 1 ) โˆˆ โ„ค )
69 11 68 45 syl2an โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) โˆˆ โ„•0 )
70 1 3 39 69 58 mulgnn0cld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) ) โ†’ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) โˆˆ ๐‘† )
71 eqid โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) = ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) )
72 eqid โŠข ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) = ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) )
73 1 4 65 66 67 70 71 72 gsummptfidmadd โŠข ( ๐œ‘ โ†’ ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) + ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) = ( ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) + ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) )
74 63 73 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) = ( ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) + ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) )
75 74 adantr โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) = ( ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) + ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ๐‘ C ( ๐‘˜ โˆ’ 1 ) ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) ) )
76 15 34 75 3eqtr4d โŠข ( ( ๐œ‘ โˆง ๐œ“ ) โ†’ ( ( ๐‘ + 1 ) โ†‘ ( ๐ด + ๐ต ) ) = ( ๐‘… ฮฃg ( ๐‘˜ โˆˆ ( 0 ... ( ๐‘ + 1 ) ) โ†ฆ ( ( ( ๐‘ + 1 ) C ๐‘˜ ) ยท ( ( ( ( ๐‘ + 1 ) โˆ’ ๐‘˜ ) โ†‘ ๐ด ) ร— ( ๐‘˜ โ†‘ ๐ต ) ) ) ) ) )