Metamath Proof Explorer

Theorem pmatcollpw3fi1lem2

Description: Lemma 2 for pmatcollpw3fi1 . (Contributed by AV, 6-Nov-2019) (Revised by AV, 4-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
pmatcollpw.c โŠข ๐ถ = ( ๐‘ Mat ๐‘ƒ )
pmatcollpw.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
pmatcollpw.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ถ )
pmatcollpw.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
pmatcollpw.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
pmatcollpw.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
pmatcollpw3.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
pmatcollpw3.d โŠข ๐ท = ( Base โ€˜ ๐ด )
Assertion pmatcollpw3fi1lem2 ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m { 0 } ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p โŠข ๐‘ƒ = ( Poly1 โ€˜ ๐‘… )
2 pmatcollpw.c โŠข ๐ถ = ( ๐‘ Mat ๐‘ƒ )
3 pmatcollpw.b โŠข ๐ต = ( Base โ€˜ ๐ถ )
4 pmatcollpw.m โŠข โˆ— = ( ยท๐‘  โ€˜ ๐ถ )
5 pmatcollpw.e โŠข โ†‘ = ( .g โ€˜ ( mulGrp โ€˜ ๐‘ƒ ) )
6 pmatcollpw.x โŠข ๐‘‹ = ( var1 โ€˜ ๐‘… )
7 pmatcollpw.t โŠข ๐‘‡ = ( ๐‘ matToPolyMat ๐‘… )
8 pmatcollpw3.a โŠข ๐ด = ( ๐‘ Mat ๐‘… )
9 pmatcollpw3.d โŠข ๐ท = ( Base โ€˜ ๐ด )
10 fveq1 โŠข ( ๐‘“ = ๐‘” โ†’ ( ๐‘“ โ€˜ ๐‘› ) = ( ๐‘” โ€˜ ๐‘› ) )
11 10 fveq2d โŠข ( ๐‘“ = ๐‘” โ†’ ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) = ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) )
12 11 oveq2d โŠข ( ๐‘“ = ๐‘” โ†’ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) = ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) )
13 12 mpteq2dv โŠข ( ๐‘“ = ๐‘” โ†’ ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) = ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) )
14 13 oveq2d โŠข ( ๐‘“ = ๐‘” โ†’ ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) )
15 14 eqeq2d โŠข ( ๐‘“ = ๐‘” โ†’ ( ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) )
16 15 cbvrexvw โŠข ( โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m { 0 } ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” โˆƒ ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) )
17 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
18 17 anim2i โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
19 18 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
20 19 ad2antrr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) )
21 simplr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) )
22 simpr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) )
23 eqid โŠข ( 0g โ€˜ ๐ด ) = ( 0g โ€˜ ๐ด )
24 eqid โŠข ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) )
25 1 2 3 4 5 6 7 8 9 23 24 pmatcollpw3fi1lem1 โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) )
26 20 21 22 25 syl3anc โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) )
27 1nn โŠข 1 โˆˆ โ„•
28 27 a1i โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) โ†’ 1 โˆˆ โ„• )
29 oveq2 โŠข ( ๐‘  = 1 โ†’ ( 0 ... ๐‘  ) = ( 0 ... 1 ) )
30 29 oveq2d โŠข ( ๐‘  = 1 โ†’ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) = ( ๐ท โ†‘m ( 0 ... 1 ) ) )
31 29 mpteq1d โŠข ( ๐‘  = 1 โ†’ ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) = ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) )
32 31 oveq2d โŠข ( ๐‘  = 1 โ†’ ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) )
33 32 eqeq2d โŠข ( ๐‘  = 1 โ†’ ( ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )
34 30 33 rexeqbidv โŠข ( ๐‘  = 1 โ†’ ( โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )
35 34 adantl โŠข ( ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘  = 1 ) โ†’ ( โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )
36 elmapi โŠข ( ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) โ†’ ๐‘” : { 0 } โŸถ ๐ท )
37 c0ex โŠข 0 โˆˆ V
38 37 snid โŠข 0 โˆˆ { 0 }
39 38 a1i โŠข ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†’ 0 โˆˆ { 0 } )
40 ffvelcdm โŠข ( ( ๐‘” : { 0 } โŸถ ๐ท โˆง 0 โˆˆ { 0 } ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท )
41 39 40 sylan2 โŠข ( ( ๐‘” : { 0 } โŸถ ๐ท โˆง ๐‘™ โˆˆ ( 0 ... 1 ) ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท )
42 41 ex โŠข ( ๐‘” : { 0 } โŸถ ๐ท โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท ) )
43 36 42 syl โŠข ( ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท ) )
44 43 adantl โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท ) )
45 44 imp โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘™ โˆˆ ( 0 ... 1 ) ) โ†’ ( ๐‘” โ€˜ 0 ) โˆˆ ๐ท )
46 8 matring โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ Ring ) โ†’ ๐ด โˆˆ Ring )
47 17 46 sylan2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing ) โ†’ ๐ด โˆˆ Ring )
48 47 3adant3 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ๐ด โˆˆ Ring )
49 9 23 ring0cl โŠข ( ๐ด โˆˆ Ring โ†’ ( 0g โ€˜ ๐ด ) โˆˆ ๐ท )
50 48 49 syl โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( 0g โ€˜ ๐ด ) โˆˆ ๐ท )
51 50 ad2antrr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘™ โˆˆ ( 0 ... 1 ) ) โ†’ ( 0g โ€˜ ๐ด ) โˆˆ ๐ท )
52 45 51 ifcld โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘™ โˆˆ ( 0 ... 1 ) ) โ†’ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) โˆˆ ๐ท )
53 52 fmpttd โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) : ( 0 ... 1 ) โŸถ ๐ท )
54 9 fvexi โŠข ๐ท โˆˆ V
55 ovex โŠข ( 0 ... 1 ) โˆˆ V
56 54 55 pm3.2i โŠข ( ๐ท โˆˆ V โˆง ( 0 ... 1 ) โˆˆ V )
57 elmapg โŠข ( ( ๐ท โˆˆ V โˆง ( 0 ... 1 ) โˆˆ V ) โ†’ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) โ†” ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) : ( 0 ... 1 ) โŸถ ๐ท ) )
58 56 57 mp1i โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โ†’ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) โ†” ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) : ( 0 ... 1 ) โŸถ ๐ท ) )
59 53 58 mpbird โŠข ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) )
60 59 adantr โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) )
61 fveq1 โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ๐‘“ โ€˜ ๐‘› ) = ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) )
62 61 fveq2d โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) = ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) )
63 62 oveq2d โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) = ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) )
64 63 mpteq2dv โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) = ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) )
65 64 oveq2d โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) )
66 65 eqeq2d โŠข ( ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ†’ ( ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) )
67 66 adantl โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘“ = ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) ) โ†’ ( ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†” ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) )
68 60 67 rspcedv โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ ( ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) โ†’ โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )
69 68 imp โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) โ†’ โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... 1 ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) )
70 28 35 69 rspcedvd โŠข ( ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... 1 ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ( ๐‘™ โˆˆ ( 0 ... 1 ) โ†ฆ if ( ๐‘™ = 0 , ( ๐‘” โ€˜ 0 ) , ( 0g โ€˜ ๐ด ) ) ) โ€˜ ๐‘› ) ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) )
71 26 70 mpdan โŠข ( ( ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โˆง ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ) โˆง ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) )
72 71 rexlimdva2 โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( โˆƒ ๐‘” โˆˆ ( ๐ท โ†‘m { 0 } ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘” โ€˜ ๐‘› ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )
73 16 72 biimtrid โŠข ( ( ๐‘ โˆˆ Fin โˆง ๐‘… โˆˆ CRing โˆง ๐‘€ โˆˆ ๐ต ) โ†’ ( โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m { 0 } ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ { 0 } โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) โ†’ โˆƒ ๐‘  โˆˆ โ„• โˆƒ ๐‘“ โˆˆ ( ๐ท โ†‘m ( 0 ... ๐‘  ) ) ๐‘€ = ( ๐ถ ฮฃg ( ๐‘› โˆˆ ( 0 ... ๐‘  ) โ†ฆ ( ( ๐‘› โ†‘ ๐‘‹ ) โˆ— ( ๐‘‡ โ€˜ ( ๐‘“ โ€˜ ๐‘› ) ) ) ) ) ) )