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 ffvelrn ⊢ ( ( 𝑔 : { 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 syl5bi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ∃ 𝑓 ∈ ( 𝐷 ↑m { 0 } ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ { 0 } ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) → ∃ 𝑠 ∈ ℕ ∃ 𝑓 ∈ ( 𝐷 ↑m ( 0 ... 𝑠 ) ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ ( 0 ... 𝑠 ) ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )