Metamath Proof Explorer


Theorem chfacfscmulgsum

Description: Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019)

Ref Expression
Hypotheses chfacfisf.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
chfacfisf.b โŠข ๐ต = ( Base โ€˜ ๐ด )
chfacfisf.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
chfacfisf.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
chfacfisf.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
chfacfisf.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
chfacfisf.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
chfacfisf.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
chfacfisf.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
chfacfscmulcl.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
chfacfscmulcl.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
chfacfscmulcl.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
chfacfscmulgsum.p โŠข + = ( +g โ€˜ ๐‘Œ )
Assertion chfacfscmulgsum ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) + ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chfacfisf.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
2 chfacfisf.b โŠข ๐ต = ( Base โ€˜ ๐ด )
3 chfacfisf.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
4 chfacfisf.y โŠข ๐‘Œ = ( ๐‘ Mat ๐‘ƒ )
5 chfacfisf.r โŠข ร— = ( .r โ€˜ ๐‘Œ )
6 chfacfisf.s โŠข โˆ’ = ( -g โ€˜ ๐‘Œ )
7 chfacfisf.0 โŠข 0 = ( 0g โ€˜ ๐‘Œ )
8 chfacfisf.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
9 chfacfisf.g โŠข ๐บ = ( ๐‘› โˆˆ โ„•0 โ†ฆ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) )
10 chfacfscmulcl.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
11 chfacfscmulcl.m โŠข ยท = ( ยท๐‘  โ€˜ ๐‘Œ )
12 chfacfscmulcl.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
13 chfacfscmulgsum.p โŠข + = ( +g โ€˜ ๐‘Œ )
14 eqid โŠข ( Base โ€˜ ๐‘Œ ) = ( Base โ€˜ ๐‘Œ )
15 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
16 15 anim2i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
17 16 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
18 3 4 pmatring โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ๐‘Œ โˆˆ Ring )
19 17 18 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ Ring )
20 ringcmn โŠข ( ๐‘Œ โˆˆ Ring โ†’ ๐‘Œ โˆˆ CMnd )
21 19 20 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ CMnd )
22 21 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘Œ โˆˆ CMnd )
23 nn0ex โŠข โ„•0 โˆˆ V
24 23 a1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ โ„•0 โˆˆ V )
25 simpll โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) )
26 simplr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) )
27 simpr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ๐‘– โˆˆ โ„•0 )
28 25 26 27 3jca โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
30 28 29 syl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
31 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulfsupp โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) finSupp 0 )
32 nn0disj โŠข ( ( 0 ... ( ๐‘  + 1 ) ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) = โˆ…
33 32 a1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( 0 ... ( ๐‘  + 1 ) ) โˆฉ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) = โˆ… )
34 nnnn0 โŠข ( ๐‘  โˆˆ โ„• โ†’ ๐‘  โˆˆ โ„•0 )
35 peano2nn0 โŠข ( ๐‘  โˆˆ โ„•0 โ†’ ( ๐‘  + 1 ) โˆˆ โ„•0 )
36 34 35 syl โŠข ( ๐‘  โˆˆ โ„• โ†’ ( ๐‘  + 1 ) โˆˆ โ„•0 )
37 nn0split โŠข ( ( ๐‘  + 1 ) โˆˆ โ„•0 โ†’ โ„•0 = ( ( 0 ... ( ๐‘  + 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) )
38 36 37 syl โŠข ( ๐‘  โˆˆ โ„• โ†’ โ„•0 = ( ( 0 ... ( ๐‘  + 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) )
39 38 ad2antrl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ โ„•0 = ( ( 0 ... ( ๐‘  + 1 ) ) โˆช ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) )
40 14 7 13 22 24 30 31 33 39 gsumsplit2 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) )
41 simpll โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) )
42 simplr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) โ†’ ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) )
43 nncn โŠข ( ๐‘  โˆˆ โ„• โ†’ ๐‘  โˆˆ โ„‚ )
44 add1p1 โŠข ( ๐‘  โˆˆ โ„‚ โ†’ ( ( ๐‘  + 1 ) + 1 ) = ( ๐‘  + 2 ) )
45 43 44 syl โŠข ( ๐‘  โˆˆ โ„• โ†’ ( ( ๐‘  + 1 ) + 1 ) = ( ๐‘  + 2 ) )
46 45 ad2antrl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘  + 1 ) + 1 ) = ( ๐‘  + 2 ) )
47 46 fveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) = ( โ„คโ‰ฅ โ€˜ ( ๐‘  + 2 ) ) )
48 47 eleq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†” ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘  + 2 ) ) ) )
49 48 biimpa โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) โ†’ ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘  + 2 ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmul0 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ๐‘  + 2 ) ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) = 0 )
51 41 42 49 50 syl3anc โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) = 0 )
52 51 mpteq2dva โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) = ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ 0 ) )
53 52 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ 0 ) ) )
54 15 18 sylan2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐‘Œ โˆˆ Ring )
55 ringmnd โŠข ( ๐‘Œ โˆˆ Ring โ†’ ๐‘Œ โˆˆ Mnd )
56 54 55 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐‘Œ โˆˆ Mnd )
57 56 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ Mnd )
58 fvex โŠข ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โˆˆ V
59 57 58 jctir โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘Œ โˆˆ Mnd โˆง ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โˆˆ V ) )
60 59 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ โˆˆ Mnd โˆง ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โˆˆ V ) )
61 7 gsumz โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โˆˆ V ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ 0 ) ) = 0 )
62 60 61 syl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ 0 ) ) = 0 )
63 53 62 eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = 0 )
64 63 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + 0 ) )
65 fzfid โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( 0 ... ( ๐‘  + 1 ) ) โˆˆ Fin )
66 elfznn0 โŠข ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†’ ๐‘– โˆˆ โ„•0 )
67 66 28 sylan2 โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) ) โ†’ ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ๐‘– โˆˆ โ„•0 ) )
68 67 29 syl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
69 68 ralrimiva โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ โˆ€ ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
70 14 22 65 69 gsummptcl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
71 14 13 7 mndrid โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + 0 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
72 57 70 71 syl2an2r โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + 0 ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
73 64 72 eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( ๐‘  + 1 ) + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) )
74 34 ad2antrl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘  โˆˆ โ„•0 )
75 14 13 22 74 68 gsummptfzsplit โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { ( ๐‘  + 1 ) } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) )
76 elfznn0 โŠข ( ๐‘– โˆˆ ( 0 ... ๐‘  ) โ†’ ๐‘– โˆˆ โ„•0 )
77 76 30 sylan2 โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 0 ... ๐‘  ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
78 14 13 22 74 77 gsummptfzsplitl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { 0 } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) )
79 57 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘Œ โˆˆ Mnd )
80 0nn0 โŠข 0 โˆˆ โ„•0
81 80 a1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ 0 โˆˆ โ„•0 )
82 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง 0 โˆˆ โ„•0 ) โ†’ ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
83 81 82 mpd3an3 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
84 oveq1 โŠข ( ๐‘– = 0 โ†’ ( ๐‘– โ†‘ ๐‘‹ ) = ( 0 โ†‘ ๐‘‹ ) )
85 fveq2 โŠข ( ๐‘– = 0 โ†’ ( ๐บ โ€˜ ๐‘– ) = ( ๐บ โ€˜ 0 ) )
86 84 85 oveq12d โŠข ( ๐‘– = 0 โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) = ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) )
87 14 86 gsumsn โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง 0 โˆˆ โ„•0 โˆง ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { 0 } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) )
88 79 81 83 87 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { 0 } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) )
89 88 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { 0 } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) )
90 78 89 eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) )
91 ovexd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘  + 1 ) โˆˆ V )
92 1nn0 โŠข 1 โˆˆ โ„•0
93 92 a1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ 1 โˆˆ โ„•0 )
94 74 93 nn0addcld โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘  + 1 ) โˆˆ โ„•0 )
95 1 2 3 4 5 6 7 8 9 10 11 12 chfacfscmulcl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โˆง ( ๐‘  + 1 ) โˆˆ โ„•0 ) โ†’ ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
96 94 95 mpd3an3 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
97 oveq1 โŠข ( ๐‘– = ( ๐‘  + 1 ) โ†’ ( ๐‘– โ†‘ ๐‘‹ ) = ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) )
98 fveq2 โŠข ( ๐‘– = ( ๐‘  + 1 ) โ†’ ( ๐บ โ€˜ ๐‘– ) = ( ๐บ โ€˜ ( ๐‘  + 1 ) ) )
99 97 98 oveq12d โŠข ( ๐‘– = ( ๐‘  + 1 ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) = ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) )
100 14 99 gsumsn โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง ( ๐‘  + 1 ) โˆˆ V โˆง ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { ( ๐‘  + 1 ) } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) )
101 79 91 96 100 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { ( ๐‘  + 1 ) } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) )
102 90 101 oveq12d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ { ( ๐‘  + 1 ) } โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) ) = ( ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) )
103 fzfid โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( 1 ... ๐‘  ) โˆˆ Fin )
104 simpll โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) )
105 simplr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) )
106 elfznn โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– โˆˆ โ„• )
107 106 nnnn0d โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– โˆˆ โ„•0 )
108 107 adantl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ๐‘– โˆˆ โ„•0 )
109 104 105 108 29 syl3anc โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
110 109 ralrimiva โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘  ) ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
111 14 22 103 110 gsummptcl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
112 14 13 mndass โŠข ( ( ๐‘Œ โˆˆ Mnd โˆง ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) ) โ†’ ( ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) ) )
113 79 111 83 96 112 syl13anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) ) )
114 106 nnne0d โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– โ‰  0 )
115 114 ad2antlr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘– โ‰  0 )
116 neeq1 โŠข ( ๐‘› = ๐‘– โ†’ ( ๐‘› โ‰  0 โ†” ๐‘– โ‰  0 ) )
117 116 adantl โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ( ๐‘› โ‰  0 โ†” ๐‘– โ‰  0 ) )
118 115 117 mpbird โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘› โ‰  0 )
119 eqneqall โŠข ( ๐‘› = 0 โ†’ ( ๐‘› โ‰  0 โ†’ 0 = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) ) )
120 118 119 mpan9 โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ 0 = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) )
121 simplr โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ๐‘› = ๐‘– )
122 eqeq1 โŠข ( 0 = ๐‘› โ†’ ( 0 = ๐‘– โ†” ๐‘› = ๐‘– ) )
123 122 eqcoms โŠข ( ๐‘› = 0 โ†’ ( 0 = ๐‘– โ†” ๐‘› = ๐‘– ) )
124 123 adantl โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ( 0 = ๐‘– โ†” ๐‘› = ๐‘– ) )
125 121 124 mpbird โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ 0 = ๐‘– )
126 125 fveq2d โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ( ๐‘ โ€˜ 0 ) = ( ๐‘ โ€˜ ๐‘– ) )
127 126 fveq2d โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) )
128 127 oveq2d โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) = ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) )
129 120 128 oveq12d โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ๐‘› = 0 ) โ†’ ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
130 elfz2 โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†” ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) ) )
131 zleltp1 โŠข ( ( ๐‘– โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค ) โ†’ ( ๐‘– โ‰ค ๐‘  โ†” ๐‘– < ( ๐‘  + 1 ) ) )
132 131 ancoms โŠข ( ( ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( ๐‘– โ‰ค ๐‘  โ†” ๐‘– < ( ๐‘  + 1 ) ) )
133 132 3adant1 โŠข ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( ๐‘– โ‰ค ๐‘  โ†” ๐‘– < ( ๐‘  + 1 ) ) )
134 133 biimpcd โŠข ( ๐‘– โ‰ค ๐‘  โ†’ ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ๐‘– < ( ๐‘  + 1 ) ) )
135 134 adantl โŠข ( ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) โ†’ ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ๐‘– < ( ๐‘  + 1 ) ) )
136 135 impcom โŠข ( ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) ) โ†’ ๐‘– < ( ๐‘  + 1 ) )
137 136 orcd โŠข ( ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) ) โ†’ ( ๐‘– < ( ๐‘  + 1 ) โˆจ ( ๐‘  + 1 ) < ๐‘– ) )
138 zre โŠข ( ๐‘  โˆˆ โ„ค โ†’ ๐‘  โˆˆ โ„ )
139 1red โŠข ( ๐‘  โˆˆ โ„ค โ†’ 1 โˆˆ โ„ )
140 138 139 readdcld โŠข ( ๐‘  โˆˆ โ„ค โ†’ ( ๐‘  + 1 ) โˆˆ โ„ )
141 zre โŠข ( ๐‘– โˆˆ โ„ค โ†’ ๐‘– โˆˆ โ„ )
142 140 141 anim12ci โŠข ( ( ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( ๐‘– โˆˆ โ„ โˆง ( ๐‘  + 1 ) โˆˆ โ„ ) )
143 142 3adant1 โŠข ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( ๐‘– โˆˆ โ„ โˆง ( ๐‘  + 1 ) โˆˆ โ„ ) )
144 lttri2 โŠข ( ( ๐‘– โˆˆ โ„ โˆง ( ๐‘  + 1 ) โˆˆ โ„ ) โ†’ ( ๐‘– โ‰  ( ๐‘  + 1 ) โ†” ( ๐‘– < ( ๐‘  + 1 ) โˆจ ( ๐‘  + 1 ) < ๐‘– ) ) )
145 143 144 syl โŠข ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โ†’ ( ๐‘– โ‰  ( ๐‘  + 1 ) โ†” ( ๐‘– < ( ๐‘  + 1 ) โˆจ ( ๐‘  + 1 ) < ๐‘– ) ) )
146 145 adantr โŠข ( ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) ) โ†’ ( ๐‘– โ‰  ( ๐‘  + 1 ) โ†” ( ๐‘– < ( ๐‘  + 1 ) โˆจ ( ๐‘  + 1 ) < ๐‘– ) ) )
147 137 146 mpbird โŠข ( ( ( 1 โˆˆ โ„ค โˆง ๐‘  โˆˆ โ„ค โˆง ๐‘– โˆˆ โ„ค ) โˆง ( 1 โ‰ค ๐‘– โˆง ๐‘– โ‰ค ๐‘  ) ) โ†’ ๐‘– โ‰  ( ๐‘  + 1 ) )
148 130 147 sylbi โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– โ‰  ( ๐‘  + 1 ) )
149 148 ad2antlr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘– โ‰  ( ๐‘  + 1 ) )
150 neeq1 โŠข ( ๐‘› = ๐‘– โ†’ ( ๐‘› โ‰  ( ๐‘  + 1 ) โ†” ๐‘– โ‰  ( ๐‘  + 1 ) ) )
151 150 adantl โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ( ๐‘› โ‰  ( ๐‘  + 1 ) โ†” ๐‘– โ‰  ( ๐‘  + 1 ) ) )
152 149 151 mpbird โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘› โ‰  ( ๐‘  + 1 ) )
153 152 adantr โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โ†’ ๐‘› โ‰  ( ๐‘  + 1 ) )
154 153 neneqd โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โ†’ ยฌ ๐‘› = ( ๐‘  + 1 ) )
155 154 pm2.21d โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โ†’ ( ๐‘› = ( ๐‘  + 1 ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) )
156 155 imp โŠข ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ๐‘› = ( ๐‘  + 1 ) ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
157 106 nnred โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– โˆˆ โ„ )
158 eleq1w โŠข ( ๐‘› = ๐‘– โ†’ ( ๐‘› โˆˆ โ„ โ†” ๐‘– โˆˆ โ„ ) )
159 157 158 syl5ibrcom โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ( ๐‘› = ๐‘– โ†’ ๐‘› โˆˆ โ„ ) )
160 159 adantl โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ๐‘› = ๐‘– โ†’ ๐‘› โˆˆ โ„ ) )
161 160 imp โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘› โˆˆ โ„ )
162 74 nn0red โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘  โˆˆ โ„ )
163 162 ad2antrr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘  โˆˆ โ„ )
164 1red โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ 1 โˆˆ โ„ )
165 163 164 readdcld โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ( ๐‘  + 1 ) โˆˆ โ„ )
166 130 136 sylbi โŠข ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†’ ๐‘– < ( ๐‘  + 1 ) )
167 166 ad2antlr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘– < ( ๐‘  + 1 ) )
168 breq1 โŠข ( ๐‘› = ๐‘– โ†’ ( ๐‘› < ( ๐‘  + 1 ) โ†” ๐‘– < ( ๐‘  + 1 ) ) )
169 168 adantl โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ( ๐‘› < ( ๐‘  + 1 ) โ†” ๐‘– < ( ๐‘  + 1 ) ) )
170 167 169 mpbird โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ๐‘› < ( ๐‘  + 1 ) )
171 161 165 170 ltnsymd โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ยฌ ( ๐‘  + 1 ) < ๐‘› )
172 171 pm2.21d โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ ( ( ๐‘  + 1 ) < ๐‘› โ†’ 0 = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) )
173 172 ad2antrr โŠข ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โ†’ ( ( ๐‘  + 1 ) < ๐‘› โ†’ 0 = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) )
174 173 imp โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ( ๐‘  + 1 ) < ๐‘› ) โ†’ 0 = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
175 simp-4r โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ๐‘› = ๐‘– )
176 175 fvoveq1d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) = ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) )
177 176 fveq2d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) )
178 175 fveq2d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ๐‘ โ€˜ ๐‘› ) = ( ๐‘ โ€˜ ๐‘– ) )
179 178 fveq2d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) )
180 179 oveq2d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) = ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) )
181 177 180 oveq12d โŠข ( ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ( ๐‘  + 1 ) < ๐‘› ) โ†’ ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
182 174 181 ifeqda โŠข ( ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โˆง ยฌ ๐‘› = ( ๐‘  + 1 ) ) โ†’ if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
183 156 182 ifeqda โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โˆง ยฌ ๐‘› = 0 ) โ†’ if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
184 129 183 ifeqda โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โˆง ๐‘› = ๐‘– ) โ†’ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
185 ovexd โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) โˆˆ V )
186 9 184 108 185 fvmptd2 โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ๐บ โ€˜ ๐‘– ) = ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) )
187 186 oveq2d โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘  ) ) โ†’ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) = ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) )
188 187 mpteq2dva โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) = ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) )
189 188 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) )
190 nn0p1gt0 โŠข ( ๐‘  โˆˆ โ„•0 โ†’ 0 < ( ๐‘  + 1 ) )
191 0red โŠข ( ๐‘  โˆˆ โ„•0 โ†’ 0 โˆˆ โ„ )
192 ltne โŠข ( ( 0 โˆˆ โ„ โˆง 0 < ( ๐‘  + 1 ) ) โ†’ ( ๐‘  + 1 ) โ‰  0 )
193 191 192 sylan โŠข ( ( ๐‘  โˆˆ โ„•0 โˆง 0 < ( ๐‘  + 1 ) ) โ†’ ( ๐‘  + 1 ) โ‰  0 )
194 neeq1 โŠข ( ๐‘› = ( ๐‘  + 1 ) โ†’ ( ๐‘› โ‰  0 โ†” ( ๐‘  + 1 ) โ‰  0 ) )
195 193 194 syl5ibrcom โŠข ( ( ๐‘  โˆˆ โ„•0 โˆง 0 < ( ๐‘  + 1 ) ) โ†’ ( ๐‘› = ( ๐‘  + 1 ) โ†’ ๐‘› โ‰  0 ) )
196 34 190 195 syl2anc2 โŠข ( ๐‘  โˆˆ โ„• โ†’ ( ๐‘› = ( ๐‘  + 1 ) โ†’ ๐‘› โ‰  0 ) )
197 196 ad2antrl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘› = ( ๐‘  + 1 ) โ†’ ๐‘› โ‰  0 ) )
198 197 imp โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘› = ( ๐‘  + 1 ) ) โ†’ ๐‘› โ‰  0 )
199 eqneqall โŠข ( ๐‘› = 0 โ†’ ( ๐‘› โ‰  0 โ†’ ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) )
200 198 199 mpan9 โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘› = ( ๐‘  + 1 ) ) โˆง ๐‘› = 0 ) โ†’ ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) )
201 iftrue โŠข ( ๐‘› = ( ๐‘  + 1 ) โ†’ if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) )
202 201 ad2antlr โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘› = ( ๐‘  + 1 ) ) โˆง ยฌ ๐‘› = 0 ) โ†’ if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) )
203 200 202 ifeqda โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โˆง ๐‘› = ( ๐‘  + 1 ) ) โ†’ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) )
204 74 35 syl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘  + 1 ) โˆˆ โ„•0 )
205 fvexd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) โˆˆ V )
206 9 203 204 205 fvmptd2 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐บ โ€˜ ( ๐‘  + 1 ) ) = ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) )
207 206 oveq2d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) = ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) )
208 15 3ad2ant2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘… โˆˆ Ring )
209 eqid โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ๐‘ƒ )
210 10 3 209 vr1cl โŠข ( ๐‘… โˆˆ Ring โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
211 208 210 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘‹ โˆˆ ( Base โ€˜ ๐‘ƒ ) )
212 eqid โŠข ( mulGrp โ€˜ ๐‘ƒ ) = ( mulGrp โ€˜ ๐‘ƒ )
213 212 209 mgpbas โŠข ( Base โ€˜ ๐‘ƒ ) = ( Base โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
214 eqid โŠข ( 1r โ€˜ ๐‘ƒ ) = ( 1r โ€˜ ๐‘ƒ )
215 212 214 ringidval โŠข ( 1r โ€˜ ๐‘ƒ ) = ( 0g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
216 213 215 12 mulg0 โŠข ( ๐‘‹ โˆˆ ( Base โ€˜ ๐‘ƒ ) โ†’ ( 0 โ†‘ ๐‘‹ ) = ( 1r โ€˜ ๐‘ƒ ) )
217 211 216 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( 0 โ†‘ ๐‘‹ ) = ( 1r โ€˜ ๐‘ƒ ) )
218 3 ply1crng โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘ƒ โˆˆ CRing )
219 218 anim2i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘ƒ โˆˆ CRing ) )
220 219 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘ƒ โˆˆ CRing ) )
221 4 matsca2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘ƒ โˆˆ CRing ) โ†’ ๐‘ƒ = ( Scalar โ€˜ ๐‘Œ ) )
222 220 221 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘ƒ = ( Scalar โ€˜ ๐‘Œ ) )
223 222 fveq2d โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( 1r โ€˜ ๐‘ƒ ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) )
224 217 223 eqtrd โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( 0 โ†‘ ๐‘‹ ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) )
225 224 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( 0 โ†‘ ๐‘‹ ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) )
226 225 oveq1d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) = ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) ยท ( ๐บ โ€˜ 0 ) ) )
227 3 4 pmatlmod โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ๐‘Œ โˆˆ LMod )
228 15 227 sylan2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐‘Œ โˆˆ LMod )
229 228 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ LMod )
230 1 2 3 4 5 6 7 8 9 chfacfisf โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐บ : โ„•0 โŸถ ( Base โ€˜ ๐‘Œ ) )
231 15 230 syl3anl2 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐บ : โ„•0 โŸถ ( Base โ€˜ ๐‘Œ ) )
232 231 81 ffvelcdmd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐บ โ€˜ 0 ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
233 eqid โŠข ( Scalar โ€˜ ๐‘Œ ) = ( Scalar โ€˜ ๐‘Œ )
234 eqid โŠข ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) = ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) )
235 14 233 11 234 lmodvs1 โŠข ( ( ๐‘Œ โˆˆ LMod โˆง ( ๐บ โ€˜ 0 ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) ยท ( ๐บ โ€˜ 0 ) ) = ( ๐บ โ€˜ 0 ) )
236 229 232 235 syl2an2r โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( 1r โ€˜ ( Scalar โ€˜ ๐‘Œ ) ) ยท ( ๐บ โ€˜ 0 ) ) = ( ๐บ โ€˜ 0 ) )
237 iftrue โŠข ( ๐‘› = 0 โ†’ if ( ๐‘› = 0 , ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) , if ( ๐‘› = ( ๐‘  + 1 ) , ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) , if ( ( ๐‘  + 1 ) < ๐‘› , 0 , ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘› โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘› ) ) ) ) ) ) ) = ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) )
238 ovexd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) โˆˆ V )
239 9 237 81 238 fvmptd3 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐บ โ€˜ 0 ) = ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) )
240 226 236 239 3eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) = ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) )
241 207 240 oveq12d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) + ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
242 14 13 cmncom โŠข ( ( ๐‘Œ โˆˆ CMnd โˆง ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) )
243 22 83 96 242 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) )
244 ringgrp โŠข ( ๐‘Œ โˆˆ Ring โ†’ ๐‘Œ โˆˆ Grp )
245 19 244 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ Grp )
246 245 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘Œ โˆˆ Grp )
247 207 96 eqeltrrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
248 19 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘Œ โˆˆ Ring )
249 8 1 2 3 4 mat2pmatbas โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘‡ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
250 15 249 syl3an2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘‡ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
251 250 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘‡ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
252 simpl1 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘ โˆˆ Fin )
253 208 adantr โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘… โˆˆ Ring )
254 elmapi โŠข ( ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) โ†’ ๐‘ : ( 0 ... ๐‘  ) โŸถ ๐ต )
255 254 adantl โŠข ( ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) โ†’ ๐‘ : ( 0 ... ๐‘  ) โŸถ ๐ต )
256 255 adantl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ๐‘ : ( 0 ... ๐‘  ) โŸถ ๐ต )
257 0elfz โŠข ( ๐‘  โˆˆ โ„•0 โ†’ 0 โˆˆ ( 0 ... ๐‘  ) )
258 34 257 syl โŠข ( ๐‘  โˆˆ โ„• โ†’ 0 โˆˆ ( 0 ... ๐‘  ) )
259 258 ad2antrl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ 0 โˆˆ ( 0 ... ๐‘  ) )
260 256 259 ffvelcdmd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘ โ€˜ 0 ) โˆˆ ๐ต )
261 8 1 2 3 4 mat2pmatbas โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring โˆง ( ๐‘ โ€˜ 0 ) โˆˆ ๐ต ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
262 252 253 260 261 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
263 14 5 ringcl โŠข ( ( ๐‘Œ โˆˆ Ring โˆง ( ๐‘‡ โ€˜ ๐‘€ ) โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
264 248 251 262 263 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) )
265 14 7 6 13 grpsubadd0sub โŠข ( ( ๐‘Œ โˆˆ Grp โˆง ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) โˆง ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) โˆˆ ( Base โ€˜ ๐‘Œ ) ) โ†’ ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) + ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
266 246 247 264 265 syl3anc โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) + ( 0 โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
267 241 243 266 3eqtr4d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) )
268 189 267 oveq12d โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) + ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
269 113 268 eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) + ( ( 0 โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ 0 ) ) ) + ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ( ๐‘  + 1 ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) + ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
270 75 102 269 3eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 0 ... ( ๐‘  + 1 ) ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) + ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )
271 40 73 270 3eqtrd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ( ๐‘  โˆˆ โ„• โˆง ๐‘ โˆˆ ( ๐ต โ†‘m ( 0 ... ๐‘  ) ) ) ) โ†’ ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ โ„•0 โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ๐บ โ€˜ ๐‘– ) ) ) ) = ( ( ๐‘Œ ฮฃg ( ๐‘– โˆˆ ( 1 ... ๐‘  ) โ†ฆ ( ( ๐‘– โ†‘ ๐‘‹ ) ยท ( ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ( ๐‘– โˆ’ 1 ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘– ) ) ) ) ) ) ) + ( ( ( ( ๐‘  + 1 ) โ†‘ ๐‘‹ ) ยท ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ ๐‘  ) ) ) โˆ’ ( ( ๐‘‡ โ€˜ ๐‘€ ) ร— ( ๐‘‡ โ€˜ ( ๐‘ โ€˜ 0 ) ) ) ) ) )